harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem all_guard (p : α → Prop) [DecidablePred p] (a : α) :
    Option.all q (guard p a) = (!p a || q a)

Proof state:
α : Type u_1
q : α → Bool
p : α → Prop
inst✝ : DecidablePred p
a : α
⊢ Option.all q (guard p a) = (!decide (p a) || q a)

Tactic:
simp only [guard]

Result:
α : Type u_1
q : α → Bool
p : α → Prop
inst✝ : DecidablePred p
a : α
⊢ Option.all q (if p a then some a else none) = (!decide (p a) || q a)

Proof state:
α : Type u_1
q : α → Bool
p : α → Prop
inst✝ : DecidablePred p
a : α
⊢ Option.all q (if p a then some a else none) = (!decide (p a) || q a)

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem _root_.Wbtw.oangle₃₁₂_eq_zero {p₁ p₂ p₃ : P} (h : Wbtw ℝ p₁ p₂ p₃) : ∡ p₃ p₁ p₂ = 0

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
⊢ ∡ p₃ p₁ p₂ = 0

Tactic:
rw [oangle_eq_zero_iff_oangle_rev_eq_zero, h.oangle₂₁₃_eq_zero]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isLittleO_congr (e : PartialHomeomorph α β) {b : β} (hb : b ∈ e.target) {f : β → E}
    {g : β → F} : f =o[𝓝 b] g ↔ (f ∘ e) =o[𝓝 (e.symm b)] (g ∘ e)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : PartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
⊢ f =o[𝓝 b] g ↔ (f ∘ ↑e) =o[𝓝 (↑e.symm b)] (g ∘ ↑e)

Tactic:
simp only [IsLittleO_def]

Result:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : PartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 b) f g) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 (↑e.symm b)) (f ∘ ↑e) (g ∘ ↑e)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : PartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 b) f g) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 (↑e.symm b)) (f ∘ ↑e) (g ∘ ↑e)

Tactic:
exact forall₂_congr fun c _hc => e.isBigOWith_congr hb

Result:
no goals
-- Mathlib/Analysis/Distribution/FourierSchwartz.lean
@[simp] lemma fourierTransformCLE_symm_apply (f : 𝓢(V, E)) :
    (fourierTransformCLE 𝕜).symm f = 𝓕⁻ f

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : RCLike 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : FiniteDimensional ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : CompleteSpace E
f : 𝓢(V, E)
⊢ ⇑((fourierTransformCLE 𝕜).symm f) = 𝓕⁻ ⇑f

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝¹⁰ : RCLike 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : FiniteDimensional ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : CompleteSpace E
f : 𝓢(V, E)
x : V
⊢ ((fourierTransformCLE 𝕜).symm f) x = 𝓕⁻ (⇑f) x

Proof state:
case h
𝕜 : Type u_1
inst✝¹⁰ : RCLike 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : FiniteDimensional ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : CompleteSpace E
f : 𝓢(V, E)
x : V
⊢ ((fourierTransformCLE 𝕜).symm f) x = 𝓕⁻ (⇑f) x

Tactic:
exact (fourierIntegralInv_eq_fourierIntegral_neg f x).symm

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma exists_lt_succ : (∃ m < n + 1, p m) ↔ (∃ m < n, p m) ∨ p n

Proof state:
n : ℕ
p : ℕ → Prop
⊢ (∃ m, m < n + 1 ∧ p m) ↔ (∃ m, m < n ∧ p m) ∨ p n

Tactic:
rw [← Decidable.not_iff_not]

Result:
n : ℕ
p : ℕ → Prop
⊢ (¬∃ m, m < n + 1 ∧ p m) ↔ ¬((∃ m, m < n ∧ p m) ∨ p n)

Proof state:
n : ℕ
p : ℕ → Prop
⊢ (∃ m, m < n + 1 ∧ p m) ↔ (∃ m, m < n ∧ p m) ∨ p n

Tactic:
classical
rw [← Decidable.not_iff_not]
simpa [not_exists, not_or] using forall_lt_succ

Result:
no goals

Proof state:
n : ℕ
p : ℕ → Prop
⊢ (¬∃ m, m < n + 1 ∧ p m) ↔ ¬((∃ m, m < n ∧ p m) ∨ p n)

Tactic:
simpa [not_exists, not_or] using forall_lt_succ

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Finite.lean
@[to_additive (attr := simp)] lemma finite_inv : s⁻¹.Finite ↔ s.Finite

Proof state:
α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
⊢ s⁻¹.Finite ↔ s.Finite

Tactic:
rw [← image_inv_eq_inv, finite_image_iff inv_injective.injOn]

Result:
no goals
-- Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
theorem finrank_eq_one_iff_of_nonzero (v : V) (nz : v ≠ 0) :
    finrank K V = 1 ↔ span K ({v} : Set V) = ⊤ :=
  ⟨fun h => by simpa using (basisSingleton Unit h v nz).span_eq, fun s =>
    finrank_eq_card_basis
      (Basis.mk (LinearIndepOn.id_singleton _ nz)
        (by
          convert s.ge  -- Porting note: added `.ge` to make things easier for `convert`
          simp))⟩

Proof state:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
nz : v ≠ 0
s : span K {v} = ⊤
⊢ ⊤ ≤ span K (Set.range fun x => id ↑x)

Tactic:
convert s.ge

Result:
case h.e'_4.h.e'_6
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
nz : v ≠ 0
s : span K {v} = ⊤
⊢ (Set.range fun x => id ↑x) = {v}

Proof state:
case h.e'_4.h.e'_6
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
nz : v ≠ 0
s : span K {v} = ⊤
⊢ (Set.range fun x => id ↑x) = {v}

Tactic:
simp

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
nz : v ≠ 0
h : finrank K V = 1
⊢ span K {v} = ⊤

Tactic:
simpa using (basisSingleton Unit h v nz).span_eq

Result:
no goals
-- Mathlib/Topology/VectorBundle/Basic.lean
theorem symm_coordChangeL (e e' : Trivialization F (π F E)) [e.IsLinear R] [e'.IsLinear R] {b : B}
    (hb : b ∈ e'.baseSet ∩ e.baseSet) : (e.coordChangeL R e' b).symm = e'.coordChangeL R e b

Proof state:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : TopologicalSpace F
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace (TotalSpace F E)
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e'.baseSet ∩ e.baseSet
⊢ (coordChangeL R e e' b).symm = coordChangeL R e' e b

Tactic:
apply ContinuousLinearEquiv.toLinearEquiv_injective

Result:
case a
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : TopologicalSpace F
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace (TotalSpace F E)
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e'.baseSet ∩ e.baseSet
⊢ (coordChangeL R e e' b).symm.toLinearEquiv = (coordChangeL R e' e b).toLinearEquiv

Proof state:
case a
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : TopologicalSpace F
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace (TotalSpace F E)
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e'.baseSet ∩ e.baseSet
⊢ (coordChangeL R e e' b).symm.toLinearEquiv = (coordChangeL R e' e b).toLinearEquiv

Tactic:
rw [coe_coordChangeL' e' e hb, (coordChangeL R e e' b).symm_toLinearEquiv,
  coe_coordChangeL' e e' hb.symm, LinearEquiv.trans_symm, LinearEquiv.symm_symm]

Result:
no goals
-- Mathlib/LinearAlgebra/Projection.lean
theorem isCompl {f : E →ₗ[R] E} (h : IsProj p f) : IsCompl p (ker f)

Proof state:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ IsCompl p (ker (codRestrict ?m.325049))

R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ IsProj ?m.324752 f

R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ Submodule R E

Tactic:
exact isCompl_of_proj h.codRestrict_apply_cod

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ IsCompl p (ker f)

Tactic:
rw [← codRestrict_ker]

Result:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ IsCompl p (ker (codRestrict ?m.325049))

R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ IsProj ?m.324752 f

R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ Submodule R E
-- Mathlib/CategoryTheory/Abelian/LeftDerived.lean
theorem NatTrans.leftDerived_id (F : C ⥤ D) [F.Additive] (n : ℕ) :
    NatTrans.leftDerived (𝟙 F) n = 𝟙 (F.leftDerived n)

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ whiskerRight (leftDerivedToHomotopyCategory (𝟙 F)) (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n) =
    𝟙 (F.leftDerived n)

Tactic:
simp only [leftDerivedToHomotopyCategory_id, whiskerRight_id']

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ 𝟙 (F.leftDerivedToHomotopyCategory ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n) = 𝟙 (F.leftDerived n)

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ leftDerived (𝟙 F) n = 𝟙 (F.leftDerived n)

Tactic:
dsimp only [leftDerived]

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ whiskerRight (leftDerivedToHomotopyCategory (𝟙 F)) (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n) =
    𝟙 (F.leftDerived n)

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ 𝟙 (F.leftDerivedToHomotopyCategory ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n) = 𝟙 (F.leftDerived n)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
theorem denom_cocycle (x y : GL(2, ℝ)⁺) (z : ℍ) :
    denom (x * y) z = denom x (smulAux y z) * denom y z

Proof state:
x y : ↥GL(2, ℝ)⁺
z : ℍ
⊢ (↑(↑↑x 1 0) * ↑(↑↑y 0 0) + ↑(↑↑x 1 1) * ↑(↑↑y 1 0)) * ↑z + (↑(↑↑x 1 0) * ↑(↑↑y 0 1) + ↑(↑↑x 1 1) * ↑(↑↑y 1 1)) =
    ↑(↑↑x 1 0) * (↑(↑↑y 0 0) * ↑z + ↑(↑↑y 0 1)) + ↑(↑↑x 1 1) * (↑(↑↑y 1 0) * ↑z + ↑(↑↑y 1 1))

Tactic:
ring

Result:
no goals

Proof state:
x y : ↥GL(2, ℝ)⁺
z : ℍ
⊢ denom (x * y) z = ↑(↑↑x 1 0) * num y z + ↑(↑↑x 1 1) * denom y z

Tactic:
simp only [denom, Subgroup.coe_mul, Fin.isValue, Units.val_mul, mul_apply, Fin.sum_univ_succ,
  Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton, Fin.succ_zero_eq_one,
  Complex.ofReal_add, Complex.ofReal_mul, num]

Result:
x y : ↥GL(2, ℝ)⁺
z : ℍ
⊢ (↑(↑↑x 1 0) * ↑(↑↑y 0 0) + ↑(↑↑x 1 1) * ↑(↑↑y 1 0)) * ↑z + (↑(↑↑x 1 0) * ↑(↑↑y 0 1) + ↑(↑↑x 1 1) * ↑(↑↑y 1 1)) =
    ↑(↑↑x 1 0) * (↑(↑↑y 0 0) * ↑z + ↑(↑↑y 0 1)) + ↑(↑↑x 1 1) * (↑(↑↑y 1 0) * ↑z + ↑(↑↑y 1 1))

Proof state:
x y : ↥GL(2, ℝ)⁺
z : ℍ
⊢ denom (x * y) z = (↑(↑↑x 1 0) * (num y z / denom y z) + ↑(↑↑x 1 1)) * denom y z

Tactic:
field_simp [denom_ne_zero]

Result:
x y : ↥GL(2, ℝ)⁺
z : ℍ
⊢ denom (x * y) z = ↑(↑↑x 1 0) * num y z + ↑(↑↑x 1 1) * denom y z

Proof state:
x y : ↥GL(2, ℝ)⁺
z : ℍ
⊢ denom (x * y) z = denom x (smulAux y z) * denom y z

Tactic:
change _ = (_ * (_ / _) + _) * _

Result:
x y : ↥GL(2, ℝ)⁺
z : ℍ
⊢ denom (x * y) z = (↑(↑↑x 1 0) * (num y z / denom y z) + ↑(↑↑x 1 1)) * denom y z
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem disjoint_sum_right {a : Multiset α} {i : Multiset (Multiset α)} :
    Disjoint a i.sum ↔ ∀ b ∈ i, Disjoint a b

Proof state:
α : Type u_3
a : Multiset α
i : Multiset (Multiset α)
⊢ Disjoint a i.sum ↔ ∀ b ∈ i, Disjoint a b

Tactic:
simpa only [disjoint_comm (a := a)] using disjoint_sum_left

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
lemma exists_lt_add_of_lt_add {x y z : ℝ≥0∞} (h : x < y + z) (hy : y ≠ 0) (hz : z ≠ 0) :
    ∃ y' < y, ∃ z' < z, x < y' + z'

Proof state:
x y z : ℝ≥0∞
h : x < y + z
hy : y ≠ 0
hz : z ≠ 0
⊢ ∃ y' < y, ∃ z' < z, x < y' + z'

Tactic:
contrapose! h

Result:
x y z : ℝ≥0∞
hy : y ≠ 0
hz : z ≠ 0
h : ∀ y' < y, ∀ z' < z, y' + z' ≤ x
⊢ y + z ≤ x

Proof state:
x y z : ℝ≥0∞
hy : y ≠ 0
hz : z ≠ 0
h : ∀ y' < y, ∀ z' < z, y' + z' ≤ x
⊢ y + z ≤ x

Tactic:
simpa using biSup_add_biSup_le' (by exact ⟨0, hy.bot_lt⟩) (by exact ⟨0, hz.bot_lt⟩) h

Result:
no goals

Proof state:
x y z : ℝ≥0∞
hy : y ≠ 0
hz : z ≠ 0
h : ∀ y' < y, ∀ z' < z, y' + z' ≤ x
⊢ ∃ i, i < y

Tactic:
exact ⟨0, hy.bot_lt⟩

Result:
no goals

Proof state:
x y z : ℝ≥0∞
hy : y ≠ 0
hz : z ≠ 0
h : ∀ y' < y, ∀ z' < z, y' + z' ≤ x
⊢ ∃ j, j < z

Tactic:
exact ⟨0, hz.bot_lt⟩

Result:
no goals
-- Mathlib/Topology/Algebra/Valued/LocallyCompact.lean
lemma _root_.Irreducible.maximalIdeal_eq_closedBall [IsDiscreteValuationRing 𝒪[K]]
    {ϖ : 𝒪[K]} (h : Irreducible ϖ) :
    (𝓂[K] : Set 𝒪[K]) = Metric.closedBall 0 ‖ϖ‖

Proof state:
K : Type u_1
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
ϖ : ↥𝒪[K]
h : Irreducible ϖ
⊢ ↑𝓂[K] = Metric.closedBall 0 ‖ϖ‖

Tactic:
rw [← coe_span_singleton_eq_closedBall, ← h.maximalIdeal_eq]

Result:
no goals
-- Mathlib/Data/Int/Star.lean
@[simp] lemma addSubmonoid_closure_range_pow {n : ℕ} (hn : Even n) :
    closure (range fun x : ℤ ↦ x ^ n) = nonneg _

Proof state:
n : ℕ
hn : Even n
⊢ closure (range fun x => x ^ n) = nonneg ℤ

Tactic:
refine le_antisymm (closure_le.2 <| range_subset_iff.2 hn.pow_nonneg) fun x hx ↦ ?_

Result:
n : ℕ
hn : Even n
x : ℤ
hx : x ∈ nonneg ℤ
⊢ x ∈ closure (range fun x => x ^ n)

Proof state:
n : ℕ
hn : Even n
x : ℤ
hx : x ∈ nonneg ℤ
⊢ x = x.natAbs • 1 ^ n

Tactic:
simpa [eq_comm (a := x)] using hx

Result:
no goals

Proof state:
n : ℕ
hn : Even n
x : ℤ
hx : x ∈ nonneg ℤ
this : x = x.natAbs • 1 ^ n
⊢ x ∈ closure (range fun x => x ^ n)

Tactic:
rw [this]

Result:
n : ℕ
hn : Even n
x : ℤ
hx : x ∈ nonneg ℤ
this : x = x.natAbs • 1 ^ n
⊢ x.natAbs • 1 ^ n ∈ closure (range fun x => x ^ n)

Proof state:
n : ℕ
hn : Even n
x : ℤ
hx : x ∈ nonneg ℤ
this : x = x.natAbs • 1 ^ n
⊢ x.natAbs • 1 ^ n ∈ closure (range fun x => x ^ n)

Tactic:
exact nsmul_mem (subset_closure <| mem_range_self _) _

Result:
no goals

Proof state:
n : ℕ
hn : Even n
x : ℤ
hx : x ∈ nonneg ℤ
⊢ x ∈ closure (range fun x => x ^ n)

Tactic:
have : x = x.natAbs • 1 ^ n := by simpa [eq_comm (a := x)] using hx

Result:
n : ℕ
hn : Even n
x : ℤ
hx : x ∈ nonneg ℤ
this : x = x.natAbs • 1 ^ n
⊢ x ∈ closure (range fun x => x ^ n)
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem mem_biUnion : J ∈ π.biUnion πi ↔ ∃ J' ∈ π, J ∈ πi J'

Proof state:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
⊢ J ∈ π.biUnion πi ↔ ∃ J' ∈ π, J ∈ πi J'

Tactic:
simp [biUnion]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Basic.lean
theorem zero_addString_eq (s : String) : (0 : Pos) + s = ⟨s.utf8ByteSize⟩

Proof state:
s : String
⊢ 0 + s = { byteIdx := s.utf8ByteSize }

Tactic:
rw [← zero_addString_byteIdx]

Result:
no goals
-- Mathlib/NumberTheory/Pell.lean
theorem y_ne_zero_of_one_lt_x {a : Solution₁ d} (ha : 1 < a.x) : a.y ≠ 0

Proof state:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
hy : a.y = 0
prop : a.x ^ 2 = 1
⊢ False

Tactic:
exact lt_irrefl _ (((one_lt_sq_iff₀ <| zero_le_one.trans ha.le).mpr ha).trans_eq prop)

Result:
no goals

Proof state:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
hy : a.y = 0
prop : a.x ^ 2 - d * a.y ^ 2 = 1
⊢ False

Tactic:
rw [hy, sq (0 : ℤ), zero_mul, mul_zero, sub_zero] at prop

Result:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
hy : a.y = 0
prop : a.x ^ 2 = 1
⊢ False

Proof state:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
⊢ a.y ≠ 0

Tactic:
intro hy

Result:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
hy : a.y = 0
⊢ False

Proof state:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
hy : a.y = 0
⊢ False

Tactic:
have prop := a.prop

Result:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
hy : a.y = 0
prop : a.x ^ 2 - d * a.y ^ 2 = 1
⊢ False
-- Mathlib/Topology/Instances/NNReal/Lemmas.lean
theorem summable_coe {f : α → ℝ≥0} : (Summable fun a => (f a : ℝ)) ↔ Summable f

Proof state:
α : Type u_1
f : α → ℝ≥0
⊢ (Summable fun a => ↑(f a)) ↔ Summable f

Tactic:
constructor

Result:
case mp
α : Type u_1
f : α → ℝ≥0
⊢ (Summable fun a => ↑(f a)) → Summable f

case mpr
α : Type u_1
f : α → ℝ≥0
⊢ Summable f → Summable fun a => ↑(f a)

Proof state:
case mp
α : Type u_1
f : α → ℝ≥0
⊢ (Summable fun a => ↑(f a)) → Summable f

Tactic:
exact fun ⟨a, ha⟩ => ⟨⟨a, ha.nonneg fun x => (f x).2⟩, hasSum_coe.1 ha⟩

Result:
no goals

Proof state:
case mpr
α : Type u_1
f : α → ℝ≥0
⊢ Summable f → Summable fun a => ↑(f a)

Tactic:
exact fun ⟨a, ha⟩ => ⟨a.1, hasSum_coe.2 ha⟩

Result:
no goals
-- Mathlib/Topology/Connected/LocPathConnected.lean
theorem IsOpen.isConnected_iff_isPathConnected {U : Set X} (U_op : IsOpen U) :
    IsConnected U ↔ IsPathConnected U

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
U : Set X
U_op : IsOpen U
⊢ IsConnected U ↔ IsPathConnected U

Tactic:
rw [isConnected_iff_connectedSpace, isPathConnected_iff_pathConnectedSpace]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
U : Set X
U_op : IsOpen U
⊢ ConnectedSpace ↑U ↔ PathConnectedSpace ↑U

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
U : Set X
U_op : IsOpen U
⊢ ConnectedSpace ↑U ↔ PathConnectedSpace ↑U

Tactic:
haveI := U_op.locPathConnectedSpace

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
U : Set X
U_op : IsOpen U
this : LocPathConnectedSpace ↑U
⊢ ConnectedSpace ↑U ↔ PathConnectedSpace ↑U

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
U : Set X
U_op : IsOpen U
this : LocPathConnectedSpace ↑U
⊢ ConnectedSpace ↑U ↔ PathConnectedSpace ↑U

Tactic:
exact pathConnectedSpace_iff_connectedSpace.symm

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Free.lean
theorem free_shortExact_finrank_add {n p : ℕ} [Module.Free R S.X₁] [Module.Free R S.X₃]
    [Module.Finite R S.X₁] [Module.Finite R S.X₃]
    (hN : Module.finrank R S.X₁ = n)
    (hP : Module.finrank R S.X₃ = p)
    [StrongRankCondition R] :
    finrank R S.X₂ = n + p

Proof state:
R : Type u_3
inst✝⁵ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
n p : ℕ
inst✝⁴ : Free R ↑S.X₁
inst✝³ : Free R ↑S.X₃
inst✝² : Module.Finite R ↑S.X₁
inst✝¹ : Module.Finite R ↑S.X₃
hN : finrank R ↑S.X₁ = n
hP : finrank R ↑S.X₃ = p
inst✝ : StrongRankCondition R
⊢ finrank R ↑S.X₂ = n + p

Tactic:
apply finrank_eq_of_rank_eq

Result:
case h
R : Type u_3
inst✝⁵ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
n p : ℕ
inst✝⁴ : Free R ↑S.X₁
inst✝³ : Free R ↑S.X₃
inst✝² : Module.Finite R ↑S.X₁
inst✝¹ : Module.Finite R ↑S.X₃
hN : finrank R ↑S.X₁ = n
hP : finrank R ↑S.X₃ = p
inst✝ : StrongRankCondition R
⊢ Module.rank R ↑S.X₂ = ↑(n + p)

Proof state:
case h
R : Type u_3
inst✝⁵ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
n p : ℕ
inst✝⁴ : Free R ↑S.X₁
inst✝³ : Free R ↑S.X₃
inst✝² : Module.Finite R ↑S.X₁
inst✝¹ : Module.Finite R ↑S.X₃
hN : finrank R ↑S.X₁ = n
hP : finrank R ↑S.X₃ = p
inst✝ : StrongRankCondition R
⊢ Module.rank R ↑S.X₂ = ↑(n + p)

Tactic:
rw [free_shortExact_rank_add hS', ← hN, ← hP]

Result:
case h
R : Type u_3
inst✝⁵ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
n p : ℕ
inst✝⁴ : Free R ↑S.X₁
inst✝³ : Free R ↑S.X₃
inst✝² : Module.Finite R ↑S.X₁
inst✝¹ : Module.Finite R ↑S.X₃
hN : finrank R ↑S.X₁ = n
hP : finrank R ↑S.X₃ = p
inst✝ : StrongRankCondition R
⊢ Module.rank R ↑S.X₁ + Module.rank R ↑S.X₃ = ↑(finrank R ↑S.X₁ + finrank R ↑S.X₃)

Proof state:
case h
R : Type u_3
inst✝⁵ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
n p : ℕ
inst✝⁴ : Free R ↑S.X₁
inst✝³ : Free R ↑S.X₃
inst✝² : Module.Finite R ↑S.X₁
inst✝¹ : Module.Finite R ↑S.X₃
hN : finrank R ↑S.X₁ = n
hP : finrank R ↑S.X₃ = p
inst✝ : StrongRankCondition R
⊢ Module.rank R ↑S.X₁ + Module.rank R ↑S.X₃ = ↑(finrank R ↑S.X₁ + finrank R ↑S.X₃)

Tactic:
simp only [Nat.cast_add, finrank_eq_rank]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean
lemma rename_esymmAlgHom (e : σ ≃ τ) :
    (renameSymmetricSubalgebra e).toAlgHom.comp (esymmAlgHom σ R n) = esymmAlgHom τ R n

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
n : ℕ
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
e : σ ≃ τ
⊢ (↑(renameSymmetricSubalgebra e)).comp (esymmAlgHom σ R n) = esymmAlgHom τ R n

Tactic:
ext i : 2

Result:
case hf.a
σ : Type u_1
τ : Type u_2
R : Type u_3
n : ℕ
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
e : σ ≃ τ
i : Fin n
⊢ ↑(((↑(renameSymmetricSubalgebra e)).comp (esymmAlgHom σ R n)) (X i)) = ↑((esymmAlgHom τ R n) (X i))

Proof state:
case hf.a
σ : Type u_1
τ : Type u_2
R : Type u_3
n : ℕ
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
e : σ ≃ τ
i : Fin n
⊢ ↑(((↑(renameSymmetricSubalgebra e)).comp (esymmAlgHom σ R n)) (X i)) = ↑((esymmAlgHom τ R n) (X i))

Tactic:
simp_rw [AlgHom.comp_apply, esymmAlgHom, aeval_X, AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_coe,
  renameSymmetricSubalgebra_apply_coe, rename_esymm]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
lemma cauchy_iInf_uniformSpace' {ι : Sort*} {u : ι → UniformSpace β}
    {l : Filter β} [l.NeBot] :
    Cauchy (uniformSpace := ⨅ i, u i) l ↔ ∀ i, Cauchy (uniformSpace := u i) l

Proof state:
β : Type v
ι : Sort u_1
u : ι → UniformSpace β
l : Filter β
inst✝ : l.NeBot
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy l

Tactic:
simp_rw [cauchy_iff_le (uniformSpace := _), iInf_uniformity, le_iInf_iff]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem cos_eq_neg_one_iff_angle_eq_pi : cos (angle x y) = -1 ↔ angle x y = π

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ cos (angle x y) = -1 ↔ angle x y = π

Tactic:
rw [← cos_pi]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ cos (angle x y) = cos π ↔ angle x y = π

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ cos (angle x y) = cos π ↔ angle x y = π

Tactic:
exact injOn_cos.eq_iff ⟨angle_nonneg x y, angle_le_pi x y⟩ (right_mem_Icc.2 pi_pos.le)

Result:
no goals