harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Multiset/UnionInter.lean
lemma sub_add_inter (s t : Multiset α) : s - t + s ∩ t = s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
⊢ ∀ (s : Multiset α), s - t + t ∩ s = s

Tactic:
refine Multiset.induction_on t (by simp) fun a t IH s => ?_

Result:
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s - t + t ∩ s = s

Tactic:
revert s

Result:
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
⊢ ∀ (s : Multiset α), s - t + t ∩ s = s

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : a ∈ s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s

Tactic:
rw [cons_inter_of_pos _ h, sub_cons, add_cons, IH, cons_erase h]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : a ∉ s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s

Tactic:
rw [cons_inter_of_neg _ h, sub_cons, erase_of_not_mem h, IH]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
⊢ ∀ (s : Multiset α), s - 0 + 0 ∩ s = s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s

Tactic:
by_cases h : a ∈ s

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : a ∈ s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s

case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : a ∉ s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s - t + s ∩ t = s

Tactic:
rw [inter_comm]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s - t + t ∩ s = s
-- Mathlib/Algebra/DirectSum/AddChar.lean
lemma directSum_injective :
    Injective (directSum : (∀ i, AddChar (G i) R) → AddChar (⨁ i, G i) R)

Proof state:
ι : Type u_1
R : Type u_2
G : ι → Type u_3
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (G i)
inst✝ : CommMonoid R
⊢ Injective directSum

Tactic:
refine toAddMonoidHomEquiv.symm.injective.comp <| DirectSum.toAddMonoid_injective.comp ?_

Result:
ι : Type u_1
R : Type u_2
G : ι → Type u_3
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (G i)
inst✝ : CommMonoid R
⊢ Injective fun ψ i => toAddMonoidHomEquiv (ψ i)

Proof state:
ι : Type u_1
R : Type u_2
G : ι → Type u_3
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (G i)
inst✝ : CommMonoid R
⊢ Injective fun ψ i => toAddMonoidHomEquiv (ψ i)

Tactic:
rintro ψ χ h

Result:
ι : Type u_1
R : Type u_2
G : ι → Type u_3
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (G i)
inst✝ : CommMonoid R
ψ χ : (i : ι) → AddChar (G i) R
h : (fun ψ i => toAddMonoidHomEquiv (ψ i)) ψ = (fun ψ i => toAddMonoidHomEquiv (ψ i)) χ
⊢ ψ = χ

Proof state:
ι : Type u_1
R : Type u_2
G : ι → Type u_3
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (G i)
inst✝ : CommMonoid R
ψ χ : (i : ι) → AddChar (G i) R
h : (fun ψ i => toAddMonoidHomEquiv (ψ i)) ψ = (fun ψ i => toAddMonoidHomEquiv (ψ i)) χ
⊢ ψ = χ

Tactic:
simpa [funext_iff] using h

Result:
no goals
-- Mathlib/FieldTheory/PrimitiveElement.lean
theorem primitive_element_inf_aux_exists_c (f g : F[X]) :
    ∃ c : F, ∀ α' ∈ (f.map ϕ).roots, ∀ β' ∈ (g.map ϕ).roots, -(α' - α) / (β' - β) ≠ ϕ c

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Infinite F
E : Type u_2
inst✝ : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
sg : Multiset E := (Polynomial.map ϕ g).roots
s : Finset E := (sf.bind fun α' => Multiset.map (fun β' => -(α' - α) / (β' - β)) sg).toFinset
⊢ ∃ c, ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ ϕ c

Tactic:
let s' := s.preimage ϕ fun x _ y _ h => ϕ.injective h

Result:
F : Type u_1
inst✝² : Field F
inst✝¹ : Infinite F
E : Type u_2
inst✝ : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
sg : Multiset E := (Polynomial.map ϕ g).roots
s : Finset E := (sf.bind fun α' => Multiset.map (fun β' => -(α' - α) / (β' - β)) sg).toFinset
s' : Finset F := s.preimage ⇑ϕ ⋯
⊢ ∃ c, ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ ϕ c
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
/-- Corollary of Chinese Remainder Theorem: if `Iᵢ` are pairwise coprime ideals in a
commutative ring then the canonical map `R → ∏ (R ⧸ Iᵢ)` is surjective. -/
lemma pi_quotient_surjective {I : ι → Ideal R}
    (hf : Pairwise fun i j ↦ IsCoprime (I i) (I j)) (x : (i : ι) → R ⧸ I i) :
    ∃ r : R, ∀ i, r = x i

Proof state:
case intro
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hf : Pairwise fun i j => IsCoprime (I i) (I j)
y : R ⧸ ⨅ i, I i
⊢ ∃ r, ∀ (i : ι), (Quotient.mk (I i)) r = (quotientInfToPiQuotient I) y i

Tactic:
obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective y

Result:
case intro.intro
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hf : Pairwise fun i j => IsCoprime (I i) (I j)
r : R
⊢ ∃ r_1, ∀ (i : ι), (Quotient.mk (I i)) r_1 = (quotientInfToPiQuotient I) ((Quotient.mk (⨅ i, I i)) r) i

Proof state:
case intro.intro
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hf : Pairwise fun i j => IsCoprime (I i) (I j)
r : R
⊢ ∃ r_1, ∀ (i : ι), (Quotient.mk (I i)) r_1 = (quotientInfToPiQuotient I) ((Quotient.mk (⨅ i, I i)) r) i

Tactic:
exact ⟨r, fun i ↦ rfl⟩

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hf : Pairwise fun i j => IsCoprime (I i) (I j)
x : (i : ι) → R ⧸ I i
⊢ ∃ r, ∀ (i : ι), (Quotient.mk (I i)) r = x i

Tactic:
obtain ⟨y, rfl⟩ := Ideal.quotientInfToPiQuotient_surj hf x

Result:
case intro
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hf : Pairwise fun i j => IsCoprime (I i) (I j)
y : R ⧸ ⨅ i, I i
⊢ ∃ r, ∀ (i : ι), (Quotient.mk (I i)) r = (quotientInfToPiQuotient I) y i
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem inv_logb_mul_base {a b : ℝ} (h₁ : a ≠ 0) (h₂ : b ≠ 0) (c : ℝ) :
    (logb (a * b) c)⁻¹ = (logb a c)⁻¹ + (logb b c)⁻¹

Proof state:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb c (a * b) = logb c a + logb c b

Tactic:
exact logb_mul h₁ h₂

Result:
no goals

Proof state:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ (logb (a * b) c)⁻¹ = (logb a c)⁻¹ + (logb b c)⁻¹

Tactic:
simp_rw [inv_logb]

Result:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb c (a * b) = logb c a + logb c b
-- Mathlib/Order/CompleteLatticeIntervals.lean
theorem coe_iInf : (↑(⨅ i, f i) : α) = a ⊓ ⨅ i, (f i : α)

Proof state:
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ a ⊓ sInf (Subtype.val '' range fun i => f i) = a ⊓ ⨅ i, ↑(f i)

Tactic:
congr

Result:
case e_a.e_a
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ (Subtype.val '' range fun i => f i) = range fun i => ↑(f i)

Proof state:
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ ↑(⨅ i, f i) = a ⊓ ⨅ i, ↑(f i)

Tactic:
rw [iInf, coe_sInf]

Result:
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ a ⊓ sInf (Subtype.val '' range fun i => f i) = a ⊓ ⨅ i, ↑(f i)

Proof state:
case e_a.e_a.h
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
x✝ : α
⊢ (x✝ ∈ Subtype.val '' range fun i => f i) ↔ x✝ ∈ range fun i => ↑(f i)

Tactic:
simp

Result:
no goals

Proof state:
case e_a.e_a
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ (Subtype.val '' range fun i => f i) = range fun i => ↑(f i)

Tactic:
ext

Result:
case e_a.e_a.h
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
x✝ : α
⊢ (x✝ ∈ Subtype.val '' range fun i => f i) ↔ x✝ ∈ range fun i => ↑(f i)
-- Mathlib/AlgebraicGeometry/Cover/Open.lean
/-- If the restriction of a global section to each member of an open cover is zero, then it is
globally zero. -/
lemma zero_of_zero_cover {X : Scheme.{u}} {U : X.Opens} (s : Γ(X, U)) (𝒰 : X.OpenCover)
    (h : ∀ i : 𝒰.J, (𝒰.map i).app U s = 0) : s = 0 :=
  𝒰.ext_elem s 0 (fun i ↦ by rw [map_zero]; exact h i)

Proof state:
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s = 0
i : 𝒰.J
⊢ (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s = 0

Tactic:
exact h i

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s = 0
i : 𝒰.J
⊢ (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s = (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) 0

Tactic:
rw [map_zero]

Result:
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s = 0
i : 𝒰.J
⊢ (ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s = 0
-- Mathlib/CategoryTheory/Sites/LocallySurjective.lean
theorem isLocallySurjective_iff_isIso {F G : Sheaf J (Type w)} (f : F ⟶ G) :
    IsLocallySurjective f ↔ IsIso (Sheaf.imageι f)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ IsLocallySurjective f ↔ IsIso (imageι f)

Tactic:
dsimp only [IsLocallySurjective]

Result:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ Presheaf.IsLocallySurjective J f.val ↔ IsIso (imageι f)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ IsIso (Subpresheaf.sheafify J (Subpresheaf.range f.val)).ι ↔
    IsIso { val := (Subpresheaf.sheafify J (Subpresheaf.range f.val)).ι }

Tactic:
exact isIso_iff_of_reflects_iso (f := Sheaf.imageι f) (F := sheafToPresheaf J (Type w))

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ Presheaf.IsLocallySurjective J f.val ↔ IsIso (imageι f)

Tactic:
rw [Sheaf.imageι, Presheaf.isLocallySurjective_iff_range_sheafify_eq_top',
  Subpresheaf.eq_top_iff_isIso]

Result:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ IsIso (Subpresheaf.sheafify J (Subpresheaf.range f.val)).ι ↔
    IsIso { val := (Subpresheaf.sheafify J (Subpresheaf.range f.val)).ι }
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_succ_X_mul (n : ℕ) (φ : R⟦X⟧) : coeff R (n + 1) (X * φ) = coeff R n φ

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (coeff R (n + 1)) (X * φ) = (coeff R n) φ

Tactic:
simp only [coeff, Finsupp.single_add, add_comm n 1]

Result:
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (MvPowerSeries.coeff R (single () 1 + single () n)) (X * φ) = (MvPowerSeries.coeff R (single () n)) φ

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (MvPowerSeries.coeff R (single () 1 + single () n)) (X * φ) = (MvPowerSeries.coeff R (single () n)) φ

Tactic:
convert φ.coeff_add_monomial_mul (single () 1) (single () n) _

Result:
case h.e'_3
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (MvPowerSeries.coeff R (single () n)) φ = 1 * (MvPowerSeries.coeff R (single () n)) φ

Proof state:
case h.e'_3
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (MvPowerSeries.coeff R (single () n)) φ = 1 * (MvPowerSeries.coeff R (single () n)) φ

Tactic:
rw [one_mul]

Result:
no goals
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem eraseLead_add_of_degree_lt_right {p q : R[X]} (pq : p.degree < q.degree) :
    (p + q).eraseLead = p + q.eraseLead

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
⊢ (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n

Tactic:
by_cases nd : n = q.natDegree

Result:
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : n = q.natDegree
⊢ (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n

case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : ¬n = q.natDegree
⊢ (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : n = q.natDegree
⊢ 0 = (p + q.eraseLead).coeff q.natDegree

Tactic:
simpa using (coeff_eq_zero_of_degree_lt (lt_of_lt_of_le pq degree_le_natDegree)).symm

Result:
no goals

Proof state:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : ¬n = q.natDegree
⊢ ¬n = (p + q).natDegree

Tactic:
rintro rfl

Result:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
nd : ¬(p + q).natDegree = q.natDegree
⊢ False

Proof state:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
nd : ¬(p + q).natDegree = q.natDegree
⊢ False

Tactic:
exact nd (natDegree_add_eq_right_of_degree_lt pq)

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : ¬n = q.natDegree
⊢ (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n

Tactic:
rw [eraseLead_coeff, coeff_add, coeff_add, eraseLead_coeff, if_neg, if_neg nd]

Result:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : ¬n = q.natDegree
⊢ ¬n = (p + q).natDegree

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : n = q.natDegree
⊢ (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n

Tactic:
rw [nd, eraseLead_coeff, if_pos (natDegree_add_eq_right_of_degree_lt pq).symm]

Result:
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : n = q.natDegree
⊢ 0 = (p + q.eraseLead).coeff q.natDegree

Proof state:
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
⊢ (p + q).eraseLead = p + q.eraseLead

Tactic:
ext n

Result:
case a
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
⊢ (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n
-- Mathlib/Algebra/Group/Opposite.lean
theorem semiconjBy_op [Mul α] {a x y : α} : SemiconjBy (op a) (op y) (op x) ↔ SemiconjBy a x y

Proof state:
α : Type u_1
inst✝ : Mul α
a x y : α
⊢ SemiconjBy (op a) (op y) (op x) ↔ SemiconjBy a x y

Tactic:
simp only [SemiconjBy, ← op_mul, op_inj, eq_comm]

Result:
no goals
-- Mathlib/FieldTheory/Perfect.lean
theorem frobenius_comp_frobeniusEquiv_symm :
    (frobenius R p).comp (frobeniusEquiv R p).symm = RingHom.id R

Proof state:
case a
R : Type u_1
p : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x✝ : R
⊢ ((frobenius R p).comp ↑(frobeniusEquiv R p).symm) x✝ = (RingHom.id R) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
p : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
⊢ (frobenius R p).comp ↑(frobeniusEquiv R p).symm = RingHom.id R

Tactic:
ext

Result:
case a
R : Type u_1
p : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x✝ : R
⊢ ((frobenius R p).comp ↑(frobeniusEquiv R p).symm) x✝ = (RingHom.id R) x✝
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
theorem tan_two_mul {z : ℂ} : tan (2 * z) = (2 : ℂ) * tan z / ((1 : ℂ) - tan z ^ 2)

Proof state:
z : ℂ
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)

Tactic:
by_cases h : ∀ k : ℤ, z ≠ (2 * k + 1) * π / 2

Result:
case pos
z : ℂ
h : ∀ (k : ℤ), z ≠ (2 * ↑k + 1) * ↑π / 2
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)

case neg
z : ℂ
h : ¬∀ (k : ℤ), z ≠ (2 * ↑k + 1) * ↑π / 2
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)

Proof state:
case neg
z : ℂ
h : ¬∀ (k : ℤ), z ≠ (2 * ↑k + 1) * ↑π / 2
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)

Tactic:
rw [not_forall_not] at h

Result:
case neg
z : ℂ
h : ∃ x, z = (2 * ↑x + 1) * ↑π / 2
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)

Proof state:
case pos
z : ℂ
h : ∀ (k : ℤ), z ≠ (2 * ↑k + 1) * ↑π / 2
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)

Tactic:
rw [two_mul, two_mul, sq, tan_add (Or.inl ⟨h, h⟩)]

Result:
no goals

Proof state:
case neg
z : ℂ
h : ∃ x, z = (2 * ↑x + 1) * ↑π / 2
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)

Tactic:
rw [two_mul, two_mul, sq, tan_add (Or.inr ⟨h, h⟩)]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/SecondInter.lean
theorem Sphere.eq_or_eq_secondInter_of_mem_mk'_span_singleton_iff_mem {s : Sphere P} {p : P}
    (hp : p ∈ s) {v : V} {p' : P} (hp' : p' ∈ AffineSubspace.mk' p (ℝ ∙ v)) :
    p' = p ∨ p' = s.secondInter p v ↔ p' ∈ s

Proof state:
case refine_2.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
hp : p ∈ s
v : V
p' : P
h : p' ∈ s
r : ℝ
hr : p' = r • v +ᵥ p
⊢ p' = p ∨ p' = s.secondInter p v

Tactic:
subst hr

Result:
case refine_2.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
hp : p ∈ s
v : V
r : ℝ
h : r • v +ᵥ p ∈ s
⊢ r • v +ᵥ p = p ∨ r • v +ᵥ p = s.secondInter p v

Proof state:
case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
hp : p ∈ s
v : V
p' : P
hp' : p' ∈ AffineSubspace.mk' p (Submodule.span ℝ {v})
h : p' ∈ s
⊢ p' = p ∨ p' = s.secondInter p v

Tactic:
rw [AffineSubspace.mem_mk'_iff_vsub_mem, Submodule.mem_span_singleton] at hp'

Result:
case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
hp : p ∈ s
v : V
p' : P
hp' : ∃ a, a • v = p' -ᵥ p
h : p' ∈ s
⊢ p' = p ∨ p' = s.secondInter p v
-- Mathlib/RingTheory/PowerBasis.lean
theorem minpolyGen_monic (pb : PowerBasis A S) : Monic (minpolyGen pb)

Proof state:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
a✝ : Nontrivial A
⊢ pb.minpolyGen.Monic

Tactic:
apply (monic_X_pow _).sub_of_left _

Result:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
a✝ : Nontrivial A
⊢ (∑ i : Fin pb.dim, C ((pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i).degree < (X ^ pb.dim).degree

Proof state:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
a✝ : Nontrivial A
⊢ (∑ i : Fin pb.dim, C ((pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i).degree < ↑pb.dim

Tactic:
exact degree_sum_fin_lt _

Result:
no goals

Proof state:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
a✝ : Nontrivial A
⊢ (∑ i : Fin pb.dim, C ((pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i).degree < (X ^ pb.dim).degree

Tactic:
rw [degree_X_pow]

Result:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
a✝ : Nontrivial A
⊢ (∑ i : Fin pb.dim, C ((pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i).degree < ↑pb.dim

Proof state:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ pb.minpolyGen.Monic

Tactic:
nontriviality A

Result:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
a✝ : Nontrivial A
⊢ pb.minpolyGen.Monic
-- Mathlib/FieldTheory/IntermediateField/Basic.lean
theorem toSubalgebra_injective : Function.Injective (toSubalgebra : IntermediateField K L → _)

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
a₁✝ a₂✝ : IntermediateField K L
h : a₁✝.toSubalgebra = a₂✝.toSubalgebra
⊢ a₁✝ = a₂✝

Tactic:
ext

Result:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
a₁✝ a₂✝ : IntermediateField K L
h : a₁✝.toSubalgebra = a₂✝.toSubalgebra
x✝ : L
⊢ x✝ ∈ a₁✝ ↔ x✝ ∈ a₂✝

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Function.Injective toSubalgebra

Tactic:
intro _ _ h

Result:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
a₁✝ a₂✝ : IntermediateField K L
h : a₁✝.toSubalgebra = a₂✝.toSubalgebra
⊢ a₁✝ = a₂✝

Proof state:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
a₁✝ a₂✝ : IntermediateField K L
h : a₁✝.toSubalgebra = a₂✝.toSubalgebra
x✝ : L
⊢ x✝ ∈ a₁✝ ↔ x✝ ∈ a₂✝

Tactic:
simp_rw [← mem_toSubalgebra, h]

Result:
no goals
-- Mathlib/Data/Matrix/Rank.lean
theorem rank_of_isUnit [StrongRankCondition R] [DecidableEq n] (A : Matrix n n R) (h : IsUnit A) :
    A.rank = Fintype.card n

Proof state:
case intro
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : DecidableEq n
A : (Matrix n n R)ˣ
⊢ (↑A).rank = Fintype.card n

Tactic:
exact rank_unit A

Result:
no goals

Proof state:
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : DecidableEq n
A : Matrix n n R
h : IsUnit A
⊢ A.rank = Fintype.card n

Tactic:
obtain ⟨A, rfl⟩ := h

Result:
case intro
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : DecidableEq n
A : (Matrix n n R)ˣ
⊢ (↑A).rank = Fintype.card n
-- Mathlib/Computability/ContextFreeGrammar.lean
theorem Language.IsContextFree.reverse (L : Language T) :
    L.IsContextFree → L.reverse.IsContextFree

Proof state:
T : Type u_1
L : Language T
⊢ L.IsContextFree → L.reverse.IsContextFree

Tactic:
rintro ⟨g, rfl⟩

Result:
case intro
T : Type u_1
g : ContextFreeGrammar T
⊢ g.language.reverse.IsContextFree

Proof state:
T : Type u_1
g : ContextFreeGrammar T
⊢ g.reverse.language = g.language.reverse

Tactic:
simp

Result:
no goals

Proof state:
case intro
T : Type u_1
g : ContextFreeGrammar T
⊢ g.language.reverse.IsContextFree

Tactic:
exact ⟨g.reverse, by simp⟩

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem mfderiv_prod_eq_add {f : M × M' → M''} {p : M × M'}
    (hf : MDifferentiableAt (I.prod I') I'' f p) :
    mfderiv (I.prod I') I'' f p =
        mfderiv (I.prod I') I'' (fun z : M × M' => f (z.1, p.2)) p +
          mfderiv (I.prod I') I'' (fun z : M × M' => f (p.1, z.2)) p

Proof state:
case h.e'_2.h.e'_24
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M × M' → M''
p : M × M'
hf : MDifferentiableAt (I.prod I') I'' f p
⊢ (ContinuousLinearMap.fst 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)).prod 0 +
      ContinuousLinearMap.prod 0 (ContinuousLinearMap.snd 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)) =
    ContinuousLinearMap.id 𝕜 (TangentSpace (I.prod I') (p.1, p.2))

Tactic:
exact ContinuousLinearMap.coprod_inl_inr

Result:
no goals