harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Lie/Weights/Basic.lean
@[ext] lemma ext {χ₁ χ₂ : Weight R L M} (h : ∀ x, χ₁ x = χ₂ x) : χ₁ = χ₂

Proof state:
case mk
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ₂ : Weight R L M
f₁ : L → R
genWeightSpace_ne_bot'✝ : genWeightSpace M f₁ ≠ ⊥
h : ∀ (x : L), { toFun := f₁, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'✝ } x = χ₂ x
⊢ { toFun := f₁, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'✝ } = χ₂

Tactic:
obtain ⟨f₂, _⟩ := χ₂

Result:
case mk.mk
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
f₁ : L → R
genWeightSpace_ne_bot'✝¹ : genWeightSpace M f₁ ≠ ⊥
f₂ : L → R
genWeightSpace_ne_bot'✝ : genWeightSpace M f₂ ≠ ⊥
h :
  ∀ (x : L),
    { toFun := f₁, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'✝¹ } x =
      { toFun := f₂, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'✝ } x
⊢ { toFun := f₁, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'✝¹ } =
    { toFun := f₂, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'✝ }

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ₁ χ₂ : Weight R L M
h : ∀ (x : L), χ₁ x = χ₂ x
⊢ χ₁ = χ₂

Tactic:
obtain ⟨f₁, _⟩ := χ₁

Result:
case mk
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ₂ : Weight R L M
f₁ : L → R
genWeightSpace_ne_bot'✝ : genWeightSpace M f₁ ≠ ⊥
h : ∀ (x : L), { toFun := f₁, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'✝ } x = χ₂ x
⊢ { toFun := f₁, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'✝ } = χ₂

Proof state:
case mk.mk
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
f₁ : L → R
genWeightSpace_ne_bot'✝¹ : genWeightSpace M f₁ ≠ ⊥
f₂ : L → R
genWeightSpace_ne_bot'✝ : genWeightSpace M f₂ ≠ ⊥
h :
  ∀ (x : L),
    { toFun := f₁, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'✝¹ } x =
      { toFun := f₂, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'✝ } x
⊢ { toFun := f₁, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'✝¹ } =
    { toFun := f₂, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'✝ }

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma toENNReal_of_nonpos {x : EReal} (hx : x ≤ 0) : x.toENNReal = 0

Proof state:
x : EReal
hx : x ≤ 0
⊢ ENNReal.ofReal x.toReal = 0

Tactic:
exact ENNReal.ofReal_of_nonpos (toReal_nonpos hx)

Result:
no goals

Proof state:
x : EReal
hx : x ≤ 0
h : x = ⊤
⊢ False

Tactic:
exact zero_ne_top <| top_le_iff.mp <| h ▸ hx

Result:
no goals

Proof state:
x : EReal
hx : x ≤ 0
⊢ x.toENNReal = 0

Tactic:
rw [toENNReal, if_neg (fun h ↦ ?_)]

Result:
x : EReal
hx : x ≤ 0
⊢ ENNReal.ofReal x.toReal = 0

x : EReal
hx : x ≤ 0
h : x = ⊤
⊢ False
-- Mathlib/Order/WellQuasiOrder.lean
theorem IsAntichain.finite_of_wellQuasiOrdered {s : Set α} (hs : IsAntichain r s)
    (hr : WellQuasiOrdered r) : s.Finite

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsAntichain r s
hr : WellQuasiOrdered r
⊢ s.Finite

Tactic:
refine Set.not_infinite.1 fun hi => ?_

Result:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsAntichain r s
hr : WellQuasiOrdered r
hi : s.Infinite
⊢ False

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsAntichain r s
hr : WellQuasiOrdered r
hi : s.Infinite
⊢ False

Tactic:
obtain ⟨m, n, hmn, h⟩ := hr fun n => hi.natEmbedding _ n

Result:
case intro.intro.intro
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsAntichain r s
hr : WellQuasiOrdered r
hi : s.Infinite
m n : ℕ
hmn : m < n
h : r ↑((Set.Infinite.natEmbedding s hi) m) ↑((Set.Infinite.natEmbedding s hi) n)
⊢ False

Proof state:
case intro.intro.intro
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsAntichain r s
hr : WellQuasiOrdered r
hi : s.Infinite
m n : ℕ
hmn : m < n
h : r ↑((Set.Infinite.natEmbedding s hi) m) ↑((Set.Infinite.natEmbedding s hi) n)
⊢ False

Tactic:
exact hmn.ne ((hi.natEmbedding _).injective <| Subtype.val_injective <|
  hs.eq (hi.natEmbedding _ m).2 (hi.natEmbedding _ n).2 h)

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem neZero' {n : ℕ} [NeZero n] (hζ : IsPrimitiveRoot ζ n) : NeZero ((n : ℕ) : R)

Proof state:
case pos.intro
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
hp : p ∣ n
k : ℕ
hk : multiplicity p n = k.succ
this✝ : NeZero p
hpri : Fact (Nat.Prime p)
this : ζ ^ n = 1
⊢ NeZero ↑n

Tactic:
rw [hm.1, hk, pow_succ', mul_assoc, pow_mul', ← frobenius_def, ← frobenius_one p] at this

Result:
case pos.intro
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
hp : p ∣ n
k : ℕ
hk : multiplicity p n = k.succ
this✝ : NeZero p
hpri : Fact (Nat.Prime p)
this : (frobenius R p) (ζ ^ (p ^ k * m)) = (frobenius R p) 1
⊢ NeZero ↑n

Proof state:
case intro
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
⊢ NeZero ↑n

Tactic:
by_cases hp : p ∣ n

Result:
case pos
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
hp : p ∣ n
⊢ NeZero ↑n

case neg
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
hp : ¬p ∣ n
⊢ NeZero ↑n

Proof state:
case pos.intro
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
hp : p ∣ n
k : ℕ
hk : multiplicity p n = k.succ
this✝ : NeZero p
hpri : Fact (Nat.Prime p)
this : (frobenius R p) (ζ ^ (p ^ k * m)) = (frobenius R p) 1
⊢ NeZero ↑n

Tactic:
exfalso

Result:
case pos.intro
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
hp : p ∣ n
k : ℕ
hk : multiplicity p n = k.succ
this✝ : NeZero p
hpri : Fact (Nat.Prime p)
this : (frobenius R p) (ζ ^ (p ^ k * m)) = (frobenius R p) 1
⊢ False
-- Mathlib/Order/Filter/Map.lean
theorem map_comap (f : Filter β) (m : α → β) : (f.comap m).map m = f ⊓ 𝓟 (range m)

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
t' t : Set β
ht : t ∈ f
sub : m ⁻¹' t ⊆ m ⁻¹' t'
x : α
hxt : m x ∈ t
⊢ m x ∈ t'

Tactic:
exact sub hxt

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
t' t : Set β
ht : t ∈ f
sub : m ⁻¹' t ⊆ m ⁻¹' t'
⊢ t ⊆ {x | x ∈ range m → x ∈ t'}

Tactic:
rintro _ hxt ⟨x, rfl⟩

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
t' t : Set β
ht : t ∈ f
sub : m ⁻¹' t ⊆ m ⁻¹' t'
x : α
hxt : m x ∈ t
⊢ m x ∈ t'

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
t' t : Set β
ht : t ∈ f
sub : m ⁻¹' t ⊆ m ⁻¹' t'
⊢ t' ∈ f ⊓ 𝓟 (range m)

Tactic:
refine mem_inf_principal.2 (mem_of_superset ht ?_)

Result:
case intro.intro
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
t' t : Set β
ht : t ∈ f
sub : m ⁻¹' t ⊆ m ⁻¹' t'
⊢ t ⊆ {x | x ∈ range m → x ∈ t'}

Proof state:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ f ⊓ 𝓟 (range m) ≤ map m (comap m f)

Tactic:
rintro t' ⟨t, ht, sub⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
t' t : Set β
ht : t ∈ f
sub : m ⁻¹' t ⊆ m ⁻¹' t'
⊢ t' ∈ f ⊓ 𝓟 (range m)

Proof state:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ map m (comap m f) = f ⊓ 𝓟 (range m)

Tactic:
refine le_antisymm (le_inf map_comap_le <| le_principal_iff.2 range_mem_map) ?_

Result:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ f ⊓ 𝓟 (range m) ≤ map m (comap m f)
-- Mathlib/RingTheory/Etale/Field.lean
theorem iff_exists_algEquiv_prod [EssFiniteType K A] :
    FormallyEtale K A ↔
      ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (_ : ∀ i, Field (Ai i))
        (_ : ∀ i, Algebra K (Ai i)) (_ : A ≃ₐ[K] Π i, Ai i),
        ∀ i, Algebra.IsSeparable K (Ai i)

Proof state:
case mp
K A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
H : FormallyEtale K A
this : Module.Finite K A
⊢ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)

Tactic:
have := FormallyUnramified.isReduced_of_field K A

Result:
case mp
K A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
H : FormallyEtale K A
this✝ : Module.Finite K A
this : IsReduced A
⊢ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)

Proof state:
case mp
K A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
H : FormallyEtale K A
⊢ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)

Tactic:
have := FormallyUnramified.finite_of_free K A

Result:
case mp
K A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
H : FormallyEtale K A
this : Module.Finite K A
⊢ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)

Proof state:
case mpr
K A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
⊢ (∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)) → FormallyEtale K A

Tactic:
intro ⟨I, _, Ai, _, _, e, _⟩

Result:
case mpr
K A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
I : Type u
w✝² : Finite I
Ai : I → Type u
w✝¹ : (i : I) → Field (Ai i)
w✝ : (i : I) → Algebra K (Ai i)
e : A ≃ₐ[K] (i : I) → Ai i
h✝ : ∀ (i : I), Algebra.IsSeparable K (Ai i)
⊢ FormallyEtale K A
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List (α × β)} {k : α}
    (contains_eq_false : (l.map Prod.fst).contains k = false)
    {h'} :
    (insertMany m l).getKey k h' =
      m.getKey k (mem_of_mem_insertMany_list h h' contains_eq_false)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List (α × β)
k : α
contains_eq_false : (List.map Prod.fst l).contains k = false
h' : k ∈ insertMany m l
⊢ (insertMany m l).getKey k h' = m.getKey k ⋯

Tactic:
simp_to_raw using Raw₀.Const.getKey_insertMany_list_of_contains_eq_false

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.bdd_mul {F : Type*} [NormedDivisionRing F] {f g : α → F} (hint : Integrable g μ)
    (hm : AEStronglyMeasurable f μ) (hfbdd : ∃ C, ∀ x, ‖f x‖ ≤ C) :
    Integrable (fun x => f x * g x) μ

Proof state:
case inr.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g μ
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
this : (fun x => ‖f x * g x‖₊) ≤ fun x => ⟨C, hCnonneg⟩ * ‖g x‖₊
⊢ ∫⁻ (a : α), ↑⟨C, hCnonneg⟩ * ↑‖g a‖₊ ∂μ < ⊤

Tactic:
rw [lintegral_const_mul' _ _ ENNReal.coe_ne_top]

Result:
case inr.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g μ
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
this : (fun x => ‖f x * g x‖₊) ≤ fun x => ⟨C, hCnonneg⟩ * ‖g x‖₊
⊢ ↑⟨C, hCnonneg⟩ * ∫⁻ (a : α), ↑‖g a‖₊ ∂μ < ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g μ
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
⊢ (fun x => ‖f x * g x‖₊) ≤ fun x => ⟨C, hCnonneg⟩ * ‖g x‖₊

Tactic:
intro x

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g μ
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
x : α
⊢ (fun x => ‖f x * g x‖₊) x ≤ (fun x => ⟨C, hCnonneg⟩ * ‖g x‖₊) x
-- Mathlib/Algebra/Group/Subgroup/Finite.lean
theorem pi_le_iff [DecidableEq η] [Finite η] {H : ∀ i, Subgroup (f i)} {J : Subgroup (∀ i, f i)} :
    pi univ H ≤ J ↔ ∀ i : η, map (MonoidHom.mulSingle f i) (H i) ≤ J

Proof state:
case mpr
η : Type u_3
f : η → Type u_4
inst✝² : (i : η) → Group (f i)
inst✝¹ : DecidableEq η
inst✝ : Finite η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
⊢ (∀ (i : η), map (MonoidHom.mulSingle f i) (H i) ≤ J) → pi univ H ≤ J

Tactic:
exact fun h x hx => pi_mem_of_mulSingle_mem x fun i => h i (mem_map_of_mem _ (hx i trivial))

Result:
no goals

Proof state:
case mp.intro.intro.a
η : Type u_3
f : η → Type u_4
inst✝² : (i : η) → Group (f i)
inst✝¹ : DecidableEq η
inst✝ : Finite η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
h : pi univ H ≤ J
i : η
x : f i
hx : x ∈ ↑(H i)
⊢ (MonoidHom.mulSingle f i) x ∈ pi univ H

Tactic:
simpa using hx

Result:
no goals

Proof state:
η : Type u_3
f : η → Type u_4
inst✝² : (i : η) → Group (f i)
inst✝¹ : DecidableEq η
inst✝ : Finite η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
⊢ pi univ H ≤ J ↔ ∀ (i : η), map (MonoidHom.mulSingle f i) (H i) ≤ J

Tactic:
constructor

Result:
case mp
η : Type u_3
f : η → Type u_4
inst✝² : (i : η) → Group (f i)
inst✝¹ : DecidableEq η
inst✝ : Finite η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
⊢ pi univ H ≤ J → ∀ (i : η), map (MonoidHom.mulSingle f i) (H i) ≤ J

case mpr
η : Type u_3
f : η → Type u_4
inst✝² : (i : η) → Group (f i)
inst✝¹ : DecidableEq η
inst✝ : Finite η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
⊢ (∀ (i : η), map (MonoidHom.mulSingle f i) (H i) ≤ J) → pi univ H ≤ J

Proof state:
case mp
η : Type u_3
f : η → Type u_4
inst✝² : (i : η) → Group (f i)
inst✝¹ : DecidableEq η
inst✝ : Finite η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
⊢ pi univ H ≤ J → ∀ (i : η), map (MonoidHom.mulSingle f i) (H i) ≤ J

Tactic:
rintro h i _ ⟨x, hx, rfl⟩

Result:
case mp.intro.intro
η : Type u_3
f : η → Type u_4
inst✝² : (i : η) → Group (f i)
inst✝¹ : DecidableEq η
inst✝ : Finite η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
h : pi univ H ≤ J
i : η
x : f i
hx : x ∈ ↑(H i)
⊢ (MonoidHom.mulSingle f i) x ∈ J

Proof state:
case mp.intro.intro
η : Type u_3
f : η → Type u_4
inst✝² : (i : η) → Group (f i)
inst✝¹ : DecidableEq η
inst✝ : Finite η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
h : pi univ H ≤ J
i : η
x : f i
hx : x ∈ ↑(H i)
⊢ (MonoidHom.mulSingle f i) x ∈ J

Tactic:
apply h

Result:
case mp.intro.intro.a
η : Type u_3
f : η → Type u_4
inst✝² : (i : η) → Group (f i)
inst✝¹ : DecidableEq η
inst✝ : Finite η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
h : pi univ H ≤ J
i : η
x : f i
hx : x ∈ ↑(H i)
⊢ (MonoidHom.mulSingle f i) x ∈ pi univ H
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem lowerBound?_eq_find? {t : RBNode α} {cut} (lb) (H : t.find? cut = some x) :
    t.lowerBound? cut lb = some x

Proof state:
α : Type u_1
x : α
t : RBNode α
cut : α → Ordering
lb : Option α
H : find? cut t.reverse.reverse = some x
⊢ upperBound? (fun x => (cut x).swap) t.reverse lb = some x

Tactic:
rw [find?_reverse] at H

Result:
α : Type u_1
x : α
t : RBNode α
cut : α → Ordering
lb : Option α
H : find? (fun x => (cut x).swap) t.reverse = some x
⊢ upperBound? (fun x => (cut x).swap) t.reverse lb = some x

Proof state:
α : Type u_1
x : α
t : RBNode α
cut : α → Ordering
lb : Option α
H : find? cut t.reverse.reverse = some x
⊢ lowerBound? cut t.reverse.reverse lb = some x

Tactic:
rw [lowerBound?_reverse]

Result:
α : Type u_1
x : α
t : RBNode α
cut : α → Ordering
lb : Option α
H : find? cut t.reverse.reverse = some x
⊢ upperBound? (fun x => (cut x).swap) t.reverse lb = some x

Proof state:
α : Type u_1
x : α
t : RBNode α
cut : α → Ordering
lb : Option α
H : find? (fun x => (cut x).swap) t.reverse = some x
⊢ upperBound? (fun x => (cut x).swap) t.reverse lb = some x

Tactic:
exact upperBound?_eq_find? _ H

Result:
no goals

Proof state:
α : Type u_1
x : α
t : RBNode α
cut : α → Ordering
lb : Option α
H : find? cut t = some x
⊢ lowerBound? cut t lb = some x

Tactic:
rw [← reverse_reverse t] at H ⊢

Result:
α : Type u_1
x : α
t : RBNode α
cut : α → Ordering
lb : Option α
H : find? cut t.reverse.reverse = some x
⊢ lowerBound? cut t.reverse.reverse lb = some x
-- Mathlib/Analysis/Complex/Angle.lean
/-- Chord-length is a multiple of arc-length up to constants. -/
lemma norm_sub_mem_Icc_angle (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) :
    ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

Proof state:
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 2 * (1 - (1 - 2 / π ^ 2 * θ ^ 2)) ≤ 2 * (1 - Real.cos θ)

Tactic:
gcongr

Result:
case h.h
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ Real.cos θ ≤ 1 - 2 / π ^ 2 * θ ^ 2

Proof state:
case intro.intro.refine_2
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (Real.cos θ - 1) ^ 2 + Real.sin θ ^ 2 ≤ θ ^ 2

Tactic:
calc
  _ = 2 * (1 - θ.cos) := by linear_combination θ.cos_sq_add_sin_sq
  _ ≤ 2 * (1 - (1 - θ ^ 2 / 2)) := by gcongr; exact Real.one_sub_sq_div_two_le_cos
  _ = _ := by ring

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem zero_pow {n : Nat} (H : 0 < n) : 0 ^ n = 0

Proof state:
n : Nat
H : 0 < 0
⊢ 0 ^ 0 = 0

Tactic:
contradiction

Result:
no goals

Proof state:
n : Nat
H : 0 < n
⊢ 0 ^ n = 0

Tactic:
match n with
| 0 => contradiction
| n+1 => rw [Nat.pow_succ, Nat.mul_zero]

Result:
no goals

Proof state:
n✝ n : Nat
H : 0 < n + 1
⊢ 0 ^ (n + 1) = 0

Tactic:
rw [Nat.pow_succ, Nat.mul_zero]

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem sphere_zero_right (n k : ℕ) : sphere (n + 1) 0 k = ∅

Proof state:
n k : ℕ
⊢ sphere (n + 1) 0 k = ∅

Tactic:
simp [sphere]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
private lemma exists_lt_mul_right_of_nonneg {a b c : α} (ha : 0 ≤ a) (hc : 0 ≤ c) (h : c < a * b) :
    ∃ b' ∈ Set.Ico 0 b, c < a * b'

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
hb : 0 < b
⊢ ∃ b' ∈ Set.Ico 0 b, c < a * b'

Tactic:
simp_rw [mul_comm a] at h ⊢

Result:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
hb : 0 < b
h : c < b * a
⊢ ∃ b' ∈ Set.Ico 0 b, c < b' * a

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
⊢ ∃ b' ∈ Set.Ico 0 b, c < a * b'

Tactic:
have hb : 0 < b := pos_of_mul_pos_right (hc.trans_lt h) ha

Result:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
hb : 0 < b
⊢ ∃ b' ∈ Set.Ico 0 b, c < a * b'

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
hb : 0 < b
h : c < b * a
⊢ ∃ b' ∈ Set.Ico 0 b, c < b' * a

Tactic:
exact exists_lt_mul_left_of_nonneg hb.le hc h

Result:
no goals
-- Mathlib/GroupTheory/FiniteAbelian/Duality.lean
private
lemma exists_apply_ne_one_aux
    (H : ∀ n : ℕ, n ∣ Monoid.exponent G → ∀ a : ZMod n, a ≠ 0 →
      ∃ φ : Multiplicative (ZMod n) →* M, φ (.ofAdd a) ≠ 1)
    {a : G} (ha : a ≠ 1) :
    ∃ φ : G →* M, φ a ≠ 1

Proof state:
case h
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
H : ∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
a : G
ha : a ≠ 1
ι : Type
w✝ : Fintype ι
n : ι → ℕ
left✝ : ∀ (i : ι), 1 < n i
h : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h.some
i : ι
hi✝ : e a i ≠ 1
hi : Multiplicative.toAdd (e a i) ≠ 0
φi : Multiplicative (ZMod (n i)) →* M
hφi : φi (Multiplicative.ofAdd (Multiplicative.toAdd (e a i))) ≠ 1
⊢ ((φi.comp (Pi.evalMonoidHom (fun i => Multiplicative (ZMod (n i))) i)).comp ↑e) a ≠ 1

Tactic:
simpa only [coe_comp, coe_coe, Function.comp_apply, Pi.evalMonoidHom_apply, ne_eq] using hφi

Result:
no goals

Proof state:
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
H : ∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
a : G
ι : Type
w✝ : Fintype ι
n : ι → ℕ
left✝ : ∀ (i : ι), 1 < n i
h : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h.some
ha : ∀ (i : ι), e a i = 1
⊢ a = 1

Tactic:
exact (MulEquiv.map_eq_one_iff e).mp <| funext ha

Result:
no goals