harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/GroupAction/Defs.lean
@[to_additive]
lemma le_stabilizer_smul_right {G'} [Group G'] [SMul α β] [MulAction G' β]
    [SMulCommClass G' α β] (a : α) (b : β) :
    stabilizer G' b ≤ stabilizer G' (a • b)

Proof state:
α : Type u_2
β : Type u_3
G' : Type u_4
inst✝³ : Group G'
inst✝² : SMul α β
inst✝¹ : MulAction G' β
inst✝ : SMulCommClass G' α β
a : α
b : β
⊢ ∀ ⦃x : G'⦄, x • b = b → a • x • b = a • b

Tactic:
rintro a h

Result:
α : Type u_2
β : Type u_3
G' : Type u_4
inst✝³ : Group G'
inst✝² : SMul α β
inst✝¹ : MulAction G' β
inst✝ : SMulCommClass G' α β
a✝ : α
b : β
a : G'
h : a • b = b
⊢ a✝ • a • b = a✝ • b

Proof state:
α : Type u_2
β : Type u_3
G' : Type u_4
inst✝³ : Group G'
inst✝² : SMul α β
inst✝¹ : MulAction G' β
inst✝ : SMulCommClass G' α β
a : α
b : β
⊢ stabilizer G' b ≤ stabilizer G' (a • b)

Tactic:
simp_rw [SetLike.le_def, mem_stabilizer_iff, smul_comm]

Result:
α : Type u_2
β : Type u_3
G' : Type u_4
inst✝³ : Group G'
inst✝² : SMul α β
inst✝¹ : MulAction G' β
inst✝ : SMulCommClass G' α β
a : α
b : β
⊢ ∀ ⦃x : G'⦄, x • b = b → a • x • b = a • b

Proof state:
α : Type u_2
β : Type u_3
G' : Type u_4
inst✝³ : Group G'
inst✝² : SMul α β
inst✝¹ : MulAction G' β
inst✝ : SMulCommClass G' α β
a✝ : α
b : β
a : G'
h : a • b = b
⊢ a✝ • a • b = a✝ • b

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Order/Monotone/MonovaryOrder.lean
lemma antivaryOn_iff_exists_antitoneOn_monotoneOn :
    AntivaryOn f g s ↔ ∃ (_ : LinearOrder ι), AntitoneOn f s ∧ MonotoneOn g s

Proof state:
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
⊢ AntivaryOn f g s ↔ ∃ x, AntitoneOn f s ∧ MonotoneOn g s

Tactic:
simp_rw [← monovaryOn_toDual_left, monovaryOn_iff_exists_monotoneOn, monotoneOn_toDual_comp_iff]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma le_traceDual_iff_map_le_one {I J : Submodule B L} :
    I ≤ Jᵛ ↔ ((I * J : Submodule B L).restrictScalars A).map
      ((trace K L).restrictScalars A) ≤ 1

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
I J : Submodule B L
⊢ I ≤ Jᵛ ↔ ∀ m ∈ restrictScalars A I, ∀ n ∈ restrictScalars A J, m * n ∈ comap (↑A (Algebra.trace K L)) 1

Tactic:
simp [SetLike.le_def, mem_traceDual]

Result:
no goals

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
I J : Submodule B L
⊢ I ≤ Jᵛ ↔ map (↑A (Algebra.trace K L)) (restrictScalars A (I * J)) ≤ 1

Tactic:
rw [Submodule.map_le_iff_le_comap, Submodule.restrictScalars_mul, Submodule.mul_le]

Result:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
I J : Submodule B L
⊢ I ≤ Jᵛ ↔ ∀ m ∈ restrictScalars A I, ∀ n ∈ restrictScalars A J, m * n ∈ comap (↑A (Algebra.trace K L)) 1
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem C_eq_two_mul_T_comp_half_mul_X [Invertible (2 : R)] (n : ℤ) :
    C R n = 2 * (T R n).comp (Polynomial.C ⅟2 * X)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this :
  (fun x => x.comp (Polynomial.C ⅟2 * X)) ((C R n).comp (2 * X)) = (fun x => x.comp (Polynomial.C ⅟2 * X)) (2 * T R n)
⊢ C R n = 2 * (T R n).comp (Polynomial.C ⅟2 * X)

Tactic:
simp_rw [comp_assoc, mul_comp, ofNat_comp, X_comp, ← mul_assoc, ← C_eq_natCast, ← C_mul,
  Nat.cast_ofNat, mul_invOf_self', map_one, one_mul, comp_X, map_ofNat] at this

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : C R n = 2 * (T R n).comp (Polynomial.C ⅟2 * X)
⊢ C R n = 2 * (T R n).comp (Polynomial.C ⅟2 * X)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : C R n = 2 * (T R n).comp (Polynomial.C ⅟2 * X)
⊢ C R n = 2 * (T R n).comp (Polynomial.C ⅟2 * X)

Tactic:
assumption

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem coe_eq_singleton {l : List α} {a : α} : (l : Multiset α) = {a} ↔ l = [a]

Proof state:
α : Type u_1
l : List α
a : α
⊢ ↑l = {a} ↔ l = [a]

Tactic:
rw [← coe_singleton, coe_eq_coe, List.perm_singleton]

Result:
no goals
-- Mathlib/GroupTheory/EckmannHilton.lean
theorem one : e₁ = e₂

Proof state:
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
⊢ e₁ = e₂

Tactic:
simpa only [h₁.left_id, h₁.right_id, h₂.left_id, h₂.right_id] using distrib e₂ e₁ e₁ e₂

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/EulerMascheroni.lean
lemma eulerMascheroniSeq_zero : eulerMascheroniSeq 0 = 0

Proof state:
⊢ eulerMascheroniSeq 0 = 0

Tactic:
simp [eulerMascheroniSeq, harmonic_zero]

Result:
no goals
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem CG.sup {N₁ N₂ : L.Substructure M} (hN₁ : N₁.CG) (hN₂ : N₂.CG) : (N₁ ⊔ N₂).CG :=
  let ⟨t₁, ht₁⟩ := cg_def.1 hN₁
  let ⟨t₂, ht₂⟩ := cg_def.1 hN₂
  cg_def.2 ⟨t₁ ∪ t₂, ht₁.1.union ht₂.1, by rw [closure_union, ht₁.2, ht₂.2]⟩

Proof state:
L : Language
M : Type u_1
inst✝ : L.Structure M
N₁ N₂ : L.Substructure M
hN₁ : N₁.CG
hN₂ : N₂.CG
t₁ : Set M
ht₁ : t₁.Countable ∧ (closure L).toFun t₁ = N₁
t₂ : Set M
ht₂ : t₂.Countable ∧ (closure L).toFun t₂ = N₂
⊢ (closure L).toFun (t₁ ∪ t₂) = N₁ ⊔ N₂

Tactic:
rw [closure_union, ht₁.2, ht₂.2]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem C_neg_two : C R (-2) = X ^ 2 - 2

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ C R (-2) = X ^ 2 - 2

Tactic:
simp [C_two]

Result:
no goals
-- Mathlib/CategoryTheory/Subterminal.lean
theorem isSubterminal_of_mono_terminal_from [HasTerminal C] [Mono (terminal.from A)] :
    IsSubterminal A := fun Z f g => by
  rw [← cancel_mono (terminal.from A)]
  subsingleton

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasTerminal C
inst✝ : Mono (terminal.from A)
Z : C
f g : Z ⟶ A
⊢ f ≫ terminal.from A = g ≫ terminal.from A

Tactic:
subsingleton

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasTerminal C
inst✝ : Mono (terminal.from A)
Z : C
f g : Z ⟶ A
⊢ f = g

Tactic:
rw [← cancel_mono (terminal.from A)]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasTerminal C
inst✝ : Mono (terminal.from A)
Z : C
f g : Z ⟶ A
⊢ f ≫ terminal.from A = g ≫ terminal.from A
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem vectorSpan_singleton (p : P) : vectorSpan k ({p} : Set P) = ⊥

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
⊢ vectorSpan k {p} = ⊥

Tactic:
simp [vectorSpan_def]

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_nat_mul (x : ℝ) (n : ℕ) : exp (n * x) = exp x ^ n :=
  ofReal_injective (by simp [exp_nat_mul])

Proof state:
x : ℝ
n : ℕ
⊢ ↑(rexp (↑n * x)) = ↑(rexp x ^ n)

Tactic:
simp [exp_nat_mul]

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
theorem iteratedDerivWithin_const_mul (c : 𝕜) {f : 𝕜 → 𝕜} (hf : ContDiffWithinAt 𝕜 n f s x) :
    iteratedDerivWithin n (fun z => c * f z) s x = c * iteratedDerivWithin n f s x

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
c : 𝕜
f : 𝕜 → 𝕜
hf : ContDiffWithinAt 𝕜 (↑n) f s x
⊢ iteratedDerivWithin n (fun z => c * f z) s x = c * iteratedDerivWithin n f s x

Tactic:
simpa using iteratedDerivWithin_const_smul (F := 𝕜) hx h c hf

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem div_const {𝕜 : Type*} {f : ℝ → 𝕜} [NormedField 𝕜] (h : IntervalIntegrable f μ a b)
    (c : 𝕜) : IntervalIntegrable (fun x => f x / c) μ a b

Proof state:
a b : ℝ
μ : Measure ℝ
𝕜 : Type u_6
f : ℝ → 𝕜
inst✝ : NormedField 𝕜
h : IntervalIntegrable f μ a b
c : 𝕜
⊢ IntervalIntegrable (fun x => f x / c) μ a b

Tactic:
simpa only [div_eq_mul_inv] using mul_const h c⁻¹

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lift_natCast (n : ℕ) : lift.{u} (n : Cardinal.{v}) = n

Proof state:
n : ℕ
⊢ lift.{u, v} ↑n = ↑n

Tactic:
induction n <;> simp [*]

Result:
no goals
-- Mathlib/Data/Nat/Pairing.lean
theorem unpair_right_le (n : ℕ) : (unpair n).2 ≤ n

Proof state:
n : ℕ
⊢ (unpair n).2 ≤ n

Tactic:
simpa using right_le_pair n.unpair.1 n.unpair.2

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Basic.lean
theorem lift_le {F : IntermediateField K L} (E : IntermediateField K F) : lift E ≤ F

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F : IntermediateField K L
E : IntermediateField K ↥F
⊢ lift E ≤ F

Tactic:
rintro _ ⟨x, _, rfl⟩

Result:
case intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F : IntermediateField K L
E : IntermediateField K ↥F
x : ↥F
left✝ : x ∈ ↑E.toSubsemiring
⊢ ↑F.val x ∈ F

Proof state:
case intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F : IntermediateField K L
E : IntermediateField K ↥F
x : ↥F
left✝ : x ∈ ↑E.toSubsemiring
⊢ ↑F.val x ∈ F

Tactic:
exact x.2

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/Simplex.lean
lemma Equilateral.dist_eq {s : Simplex R P n} (he : s.Equilateral) {i₁ i₂ i₃ i₄ : Fin (n + 1)}
    (h₁₂ : i₁ ≠ i₂) (h₃₄ : i₃ ≠ i₄) :
    dist (s.points i₁) (s.points i₂) = dist (s.points i₃) (s.points i₄)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
he : s.Equilateral
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
⊢ dist (s.points i₁) (s.points i₂) = dist (s.points i₃) (s.points i₄)

Tactic:
rcases he with ⟨r, hr⟩

Result:
case intro
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist (s.points i) (s.points j) = r
⊢ dist (s.points i₁) (s.points i₂) = dist (s.points i₃) (s.points i₄)

Proof state:
case intro
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist (s.points i) (s.points j) = r
⊢ dist (s.points i₁) (s.points i₂) = dist (s.points i₃) (s.points i₄)

Tactic:
rw [hr _ _ h₁₂, hr _ _ h₃₄]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem sInter_eq_empty_iff {c : Set (Set α)} : ⋂₀ c = ∅ ↔ ∀ a, ∃ b ∈ c, a ∉ b

Proof state:
α : Type u_1
c : Set (Set α)
⊢ ⋂₀ c = ∅ ↔ ∀ (a : α), ∃ b ∈ c, a ∉ b

Tactic:
simp [Set.eq_empty_iff_forall_not_mem]

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.nhdsSet_prod_eq_biSup {K : Set X} (hK : IsCompact K) {Y} (l : Filter Y) :
    (𝓝ˢ K) ×ˢ l = ⨆ x ∈ K, 𝓝 x ×ˢ l :=
  le_antisymm (fun s hs ↦ hK.mem_nhdsSet_prod_of_forall <| by simpa using hs)
    (iSup₂_le fun _ hx ↦ prod_mono (nhds_le_nhdsSet hx) le_rfl)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
K : Set X
hK : IsCompact K
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hs : s ∈ ⨆ x ∈ K, 𝓝 x ×ˢ l
⊢ ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l

Tactic:
simpa using hs

Result:
no goals
-- Mathlib/Order/Interval/Finset/Defs.lean
@[simp]
lemma toFinset_Iio (a : α) [Fintype (Iio a)] : (Iio a).toFinset = Finset.Iio a

Proof state:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
a : α
inst✝ : Fintype ↑(Iio a)
⊢ (Iio a).toFinset = Finset.Iio a

Tactic:
ext

Result:
case h
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
a : α
inst✝ : Fintype ↑(Iio a)
a✝ : α
⊢ a✝ ∈ (Iio a).toFinset ↔ a✝ ∈ Finset.Iio a

Proof state:
case h
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
a : α
inst✝ : Fintype ↑(Iio a)
a✝ : α
⊢ a✝ ∈ (Iio a).toFinset ↔ a✝ ∈ Finset.Iio a

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
@[simp]
lemma completedHurwitzZetaEven₀_neg (a : UnitAddCircle) (s : ℂ) :
    completedHurwitzZetaEven₀ (-a) s = completedHurwitzZetaEven₀ a s

Proof state:
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven₀ (-a) s = completedHurwitzZetaEven₀ a s

Tactic:
simp [completedHurwitzZetaEven₀]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem aleph0_le_of_isSuccLimit {c : Cardinal} (h : IsSuccLimit c) : ℵ₀ ≤ c

Proof state:
c : Cardinal.{u_1}
h : IsSuccLimit c
⊢ ℵ₀ ≤ c

Tactic:
contrapose! h

Result:
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ¬IsSuccLimit c

Proof state:
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ¬IsSuccLimit c

Tactic:
exact not_isSuccLimit_of_lt_aleph0 h

Result:
no goals
-- Mathlib/NumberTheory/FLT/Four.lean
theorem comm {a b c : ℤ} : Fermat42 a b c ↔ Fermat42 b a c

Proof state:
a b c : ℤ
⊢ Fermat42 a b c ↔ Fermat42 b a c

Tactic:
delta Fermat42

Result:
a b c : ℤ
⊢ a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2 ↔ b ≠ 0 ∧ a ≠ 0 ∧ b ^ 4 + a ^ 4 = c ^ 2

Proof state:
a b c : ℤ
⊢ a ≠ 0 ∧ b ≠ 0 ∧ b ^ 4 + a ^ 4 = c ^ 2 ↔ b ≠ 0 ∧ a ≠ 0 ∧ b ^ 4 + a ^ 4 = c ^ 2

Tactic:
tauto

Result:
no goals

Proof state:
a b c : ℤ
⊢ a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2 ↔ b ≠ 0 ∧ a ≠ 0 ∧ b ^ 4 + a ^ 4 = c ^ 2

Tactic:
rw [add_comm]

Result:
a b c : ℤ
⊢ a ≠ 0 ∧ b ≠ 0 ∧ b ^ 4 + a ^ 4 = c ^ 2 ↔ b ≠ 0 ∧ a ≠ 0 ∧ b ^ 4 + a ^ 4 = c ^ 2
-- Mathlib/Algebra/ZeroOne/Lemmas.lean
@[to_additive]
lemma ite_le_one [LE α] (ha : a ≤ 1) (hb : b ≤ 1) : ite p a b ≤ 1

Proof state:
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : a ≤ 1
hb : b ≤ 1
⊢ (if p then a else b) ≤ 1

Tactic:
split <;> assumption

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/GetElem.lean
theorem getElem?_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
    (c : cont) (i : idx) (h : dom c i) : c[i]? = some (c[i]'h)

Proof state:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝¹ : GetElem? cont idx elem dom
inst✝ : LawfulGetElem cont idx elem dom
c : cont
i : idx
h : dom c i
this : Decidable (dom c i)
⊢ (if h : dom c i then some (getElem c i h) else none) = some (getElem c i h)

Tactic:
exact dif_pos h

Result:
no goals

Proof state:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝¹ : GetElem? cont idx elem dom
inst✝ : LawfulGetElem cont idx elem dom
c : cont
i : idx
h : dom c i
this : Decidable (dom c i)
⊢ getElem? c i = some (getElem c i h)

Tactic:
rw [getElem?_def]

Result:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝¹ : GetElem? cont idx elem dom
inst✝ : LawfulGetElem cont idx elem dom
c : cont
i : idx
h : dom c i
this : Decidable (dom c i)
⊢ (if h : dom c i then some (getElem c i h) else none) = some (getElem c i h)

Proof state:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝¹ : GetElem? cont idx elem dom
inst✝ : LawfulGetElem cont idx elem dom
c : cont
i : idx
h : dom c i
⊢ getElem? c i = some (getElem c i h)

Tactic:
have : Decidable (dom c i) := .isTrue h

Result:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝¹ : GetElem? cont idx elem dom
inst✝ : LawfulGetElem cont idx elem dom
c : cont
i : idx
h : dom c i
this : Decidable (dom c i)
⊢ getElem? c i = some (getElem c i h)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_empty_iff (a : α) : a ∈ (#[] : Array α) ↔ False

Proof state:
α : Type u_1
a : α
⊢ a ∈ #[] ↔ False

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Defs.lean
theorem conj_mem' (nH : H.Normal) (n : G) (hn : n ∈ H) (g : G) :
    g⁻¹ * n * g ∈ H

Proof state:
case h.e'_5.h.e'_6
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : H.Normal
n : G
hn : n ∈ H
g : G
⊢ g = g⁻¹⁻¹

Tactic:
rw [inv_inv]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : H.Normal
n : G
hn : n ∈ H
g : G
⊢ g⁻¹ * n * g ∈ H

Tactic:
convert nH.conj_mem n hn g⁻¹

Result:
case h.e'_5.h.e'_6
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : H.Normal
n : G
hn : n ∈ H
g : G
⊢ g = g⁻¹⁻¹
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem circumradius_eq_of_cospherical {ps : Set P} {n : ℕ} [FiniteDimensional ℝ V]
    (hd : finrank ℝ V = n) (hc : Cospherical ps) {sx₁ sx₂ : Simplex ℝ P n}
    (hsx₁ : Set.range sx₁.points ⊆ ps) (hsx₂ : Set.range sx₂.points ⊆ ps) :
    sx₁.circumradius = sx₂.circumradius

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
⊢ sx₁.circumradius = sx₂.circumradius

Tactic:
rcases exists_circumradius_eq_of_cospherical hd hc with ⟨r, hr⟩

Result:
case intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : ℝ
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
⊢ sx₁.circumradius = sx₂.circumradius

Proof state:
case intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : ℝ
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
⊢ sx₁.circumradius = sx₂.circumradius

Tactic:
rw [hr sx₁ hsx₁, hr sx₂ hsx₂]

Result:
no goals
-- Mathlib/Algebra/Ring/Int/Parity.lean
theorem isSquare_natCast_iff {n : ℕ} : IsSquare (n : ℤ) ↔ IsSquare n

Proof state:
case mpr.intro
n x : ℕ
h : n = x * x
⊢ IsSquare ↑n

Tactic:
exact ⟨x, mod_cast h⟩

Result:
no goals

Proof state:
n : ℕ
⊢ IsSquare ↑n ↔ IsSquare n

Tactic:
constructor <;> rintro ⟨x, h⟩

Result:
case mp.intro
n : ℕ
x : ℤ
h : ↑n = x * x
⊢ IsSquare n

case mpr.intro
n x : ℕ
h : n = x * x
⊢ IsSquare ↑n

Proof state:
case mp.intro
n : ℕ
x : ℤ
h : ↑n = x * x
⊢ IsSquare n

Tactic:
exact ⟨x.natAbs, (natAbs_mul_natAbs_eq h.symm).symm⟩

Result:
no goals
-- Mathlib/Order/Directed.lean
theorem directedOn_iff_directed {s} : @DirectedOn α r s ↔ Directed r (Subtype.val : s → α)

Proof state:
α : Type u
r : α → α → Prop
s : Set α
⊢ (∀ x ∈ s, ∀ y ∈ s, ∃ z ∈ s, r x z ∧ r y z) ↔ ∀ a ∈ s, ∀ a_1 ∈ s, ∃ a_2, r a a_2 ∧ a_2 ∈ s ∧ r a_1 a_2

Tactic:
exact forall₂_congr fun x _ => by simp [And.comm, and_assoc]

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
s : Set α
x : α
x✝ : x ∈ s
⊢ (∀ y ∈ s, ∃ z ∈ s, r x z ∧ r y z) ↔ ∀ a ∈ s, ∃ a_1, r x a_1 ∧ a_1 ∈ s ∧ r a a_1

Tactic:
simp [And.comm, and_assoc]

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
s : Set α
⊢ DirectedOn r s ↔ Directed r Subtype.val

Tactic:
simp only [DirectedOn, Directed, Subtype.exists, exists_and_left, exists_prop, Subtype.forall]

Result:
α : Type u
r : α → α → Prop
s : Set α
⊢ (∀ x ∈ s, ∀ y ∈ s, ∃ z ∈ s, r x z ∧ r y z) ↔ ∀ a ∈ s, ∀ a_1 ∈ s, ∃ a_2, r a a_2 ∧ a_2 ∈ s ∧ r a_1 a_2
-- Mathlib/GroupTheory/SpecificGroups/Quaternion.lean
theorem xa_pow_four (i : ZMod (2 * n)) : xa i ^ 4 = 1

Proof state:
n : ℕ
i : ZMod (2 * n)
⊢ xa i ^ 4 = a (↑n + ↑n)

Tactic:
simp [pow_succ, add_sub_assoc, sub_sub_cancel]

Result:
no goals

Proof state:
n : ℕ
i : ZMod (2 * n)
⊢ xa i ^ 4 = 1

Tactic:
calc xa i ^ 4
    = a (n + n)  := by simp [pow_succ, add_sub_assoc, sub_sub_cancel]
  _ = a ↑(2 * n) := by simp [Nat.cast_add, two_mul]
  _ = 1          := by simp

Result:
no goals

Proof state:
n : ℕ
i : ZMod (2 * n)
⊢ a (↑n + ↑n) = a ↑(2 * n)

Tactic:
simp [Nat.cast_add, two_mul]

Result:
no goals

Proof state:
n : ℕ
i : ZMod (2 * n)
⊢ a ↑(2 * n) = 1

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Induced.lean
theorem trim_sum_ge {ι} (m : ι → OuterMeasure α) : (sum fun i => (m i).trim) ≤ (sum m).trim :=
  fun s => by
  simp only [sum_apply, trim_eq_iInf, le_iInf_iff]
  exact fun t st ht =>
    ENNReal.tsum_le_tsum fun i => iInf_le_of_le t <| iInf_le_of_le st <| iInf_le _ ht

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
ι : Type u_2
m : ι → OuterMeasure α
s : Set α
⊢ ∀ (i : Set α),
    s ⊆ i → MeasurableSet i → ∑' (i : ι), ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m i) t ≤ ∑' (i_3 : ι), (m i_3) i

Tactic:
exact fun t st ht =>
  ENNReal.tsum_le_tsum fun i => iInf_le_of_le t <| iInf_le_of_le st <| iInf_le _ ht

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
ι : Type u_2
m : ι → OuterMeasure α
s : Set α
⊢ (sum fun i => (m i).trim) s ≤ (sum m).trim s

Tactic:
simp only [sum_apply, trim_eq_iInf, le_iInf_iff]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
ι : Type u_2
m : ι → OuterMeasure α
s : Set α
⊢ ∀ (i : Set α),
    s ⊆ i → MeasurableSet i → ∑' (i : ι), ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m i) t ≤ ∑' (i_3 : ι), (m i_3) i
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSubOfPoint_map (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P) (b : P) :
    (s₂.map e).weightedVSubOfPoint p b w = s₂.weightedVSubOfPoint (p ∘ e) b (w ∘ e)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
w : ι → k
p : ι → P
b : P
⊢ ((map e s₂).weightedVSubOfPoint p b) w = (s₂.weightedVSubOfPoint (p ∘ ⇑e) b) (w ∘ ⇑e)

Tactic:
simp_rw [weightedVSubOfPoint_apply]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
w : ι → k
p : ι → P
b : P
⊢ ∑ i ∈ map e s₂, w i • (p i -ᵥ b) = ∑ i ∈ s₂, (w ∘ ⇑e) i • ((p ∘ ⇑e) i -ᵥ b)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
w : ι → k
p : ι → P
b : P
⊢ ∑ i ∈ map e s₂, w i • (p i -ᵥ b) = ∑ i ∈ s₂, (w ∘ ⇑e) i • ((p ∘ ⇑e) i -ᵥ b)

Tactic:
exact Finset.sum_map _ _ _

Result:
no goals