harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/SmoothSeries.lean
theorem differentiable_tsum (hu : Summable u) (hf : ∀ n x, HasFDerivAt (f n) (f' n x) x)
    (hf' : ∀ n x, ‖f' n x‖ ≤ u n) : Differentiable 𝕜 fun y => ∑' n, f n y

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
⊢ Differentiable 𝕜 fun y => ∑' (n : α), f n y

Tactic:
by_cases h : ∃ x₀, Summable fun n => f n x₀

Result:
case pos
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
h : ∃ x₀, Summable fun n => f n x₀
⊢ Differentiable 𝕜 fun y => ∑' (n : α), f n y

case neg
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
h : ¬∃ x₀, Summable fun n => f n x₀
⊢ Differentiable 𝕜 fun y => ∑' (n : α), f n y

Proof state:
case neg
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
h : ¬∃ x₀, Summable fun n => f n x₀
⊢ Differentiable 𝕜 fun y => ∑' (n : α), f n y

Tactic:
push_neg at h

Result:
case neg
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
h : ∀ (x₀ : E), ¬Summable fun n => f n x₀
⊢ Differentiable 𝕜 fun y => ∑' (n : α), f n y
-- Mathlib/Data/Sum/Basic.lean
theorem exists_of_isRight_left (h₁ : LiftRel r s x y) (h₂ : x.isRight) :
    ∃ b d, s b d ∧ x = inr b ∧ y = inr d

Proof state:
case intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
y : γ ⊕ δ
w✝ : β
h₂ : (inr w✝).isRight = true
h₁ : ∃ b d, s b d ∧ inr w✝ = inr b ∧ y = inr d
⊢ ∃ b d, s b d ∧ inr w✝ = inr b ∧ y = inr d

Tactic:
exact h₁

Result:
no goals

Proof state:
case intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
y : γ ⊕ δ
w✝ : β
h₁ : LiftRel r s (inr w✝) y
h₂ : (inr w✝).isRight = true
⊢ ∃ b d, s b d ∧ inr w✝ = inr b ∧ y = inr d

Tactic:
simp only [liftRel_iff, false_and, and_false, exists_false, false_or, reduceCtorEq] at h₁

Result:
case intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
y : γ ⊕ δ
w✝ : β
h₂ : (inr w✝).isRight = true
h₁ : ∃ b d, s b d ∧ inr w✝ = inr b ∧ y = inr d
⊢ ∃ b d, s b d ∧ inr w✝ = inr b ∧ y = inr d

Proof state:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
y : γ ⊕ δ
h₁ : LiftRel r s x y
h₂ : x.isRight = true
⊢ ∃ b d, s b d ∧ x = inr b ∧ y = inr d

Tactic:
rcases isRight_iff.mp h₂ with ⟨_, rfl⟩

Result:
case intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
y : γ ⊕ δ
w✝ : β
h₁ : LiftRel r s (inr w✝) y
h₂ : (inr w✝).isRight = true
⊢ ∃ b d, s b d ∧ inr w✝ = inr b ∧ y = inr d
-- Mathlib/RingTheory/Norm/Basic.lean
lemma norm_eq_of_algEquiv [Ring T] [Algebra R T] (e : S ≃ₐ[R] T) (x) :
    Algebra.norm R (e x) = Algebra.norm R x

Proof state:
case h.e_6.h
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
x : S
⊢ (lmul R T) (e x) = ↑e.toLinearEquiv ∘ₗ (lmul R S) x ∘ₗ ↑e.toLinearEquiv.symm

Tactic:
ext

Result:
case h.e_6.h.h
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
x : S
x✝ : T
⊢ ((lmul R T) (e x)) x✝ = (↑e.toLinearEquiv ∘ₗ (lmul R S) x ∘ₗ ↑e.toLinearEquiv.symm) x✝

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
x : S
⊢ (norm R) (e x) = (norm R) x

Tactic:
simp_rw [Algebra.norm_apply, ← LinearMap.det_conj _ e.toLinearEquiv]

Result:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
x : S
⊢ LinearMap.det ((lmul R T) (e x)) = LinearMap.det (↑e.toLinearEquiv ∘ₗ (lmul R S) x ∘ₗ ↑e.toLinearEquiv.symm)

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
x : S
⊢ LinearMap.det ((lmul R T) (e x)) = LinearMap.det (↑e.toLinearEquiv ∘ₗ (lmul R S) x ∘ₗ ↑e.toLinearEquiv.symm)

Tactic:
congr

Result:
case h.e_6.h
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
x : S
⊢ (lmul R T) (e x) = ↑e.toLinearEquiv ∘ₗ (lmul R S) x ∘ₗ ↑e.toLinearEquiv.symm

Proof state:
case h.e_6.h.h
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
x : S
x✝ : T
⊢ ((lmul R T) (e x)) x✝ = (↑e.toLinearEquiv ∘ₗ (lmul R S) x ∘ₗ ↑e.toLinearEquiv.symm) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/IsConjRoot.lean
theorem sub_algebraMap {x y : S} (r : K) (h : IsConjRoot K x y) :
    IsConjRoot K (x - algebraMap K S r) (y - algebraMap K S r)

Proof state:
K : Type u_2
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Field K
inst✝ : Algebra K S
x y : S
r : K
h : IsConjRoot K x y
⊢ IsConjRoot K (x - (algebraMap K S) r) (y - (algebraMap K S) r)

Tactic:
simpa only [sub_eq_add_neg, map_neg] using add_algebraMap (-r) h

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem quadratic_reciprocity_if {a b : ℕ} (ha2 : a % 2 = 1) (hb2 : b % 2 = 1) :
    (if a % 4 = 3 ∧ b % 4 = 3 then -J(b | a) else J(b | a)) = J(a | b)

Proof state:
case inr.inl
a b : ℕ
ha2 : a % 2 = 1
hb2 : b % 2 = 1
ha3 : a % 4 = 3
hb1 : b % 4 = 1
⊢ (if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)) = J(↑a | b)

Tactic:
simpa [hb1] using jacobiSym.quadratic_reciprocity_one_mod_four hb1 (Nat.odd_iff.mpr ha2)

Result:
no goals

Proof state:
case inr.inr
a b : ℕ
ha2 : a % 2 = 1
hb2 : b % 2 = 1
ha3 : a % 4 = 3
hb3 : b % 4 = 3
⊢ (if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)) = J(↑a | b)

Tactic:
simpa [ha3, hb3] using (jacobiSym.quadratic_reciprocity_three_mod_four ha3 hb3).symm

Result:
no goals

Proof state:
case inr
a b : ℕ
ha2 : a % 2 = 1
hb2 : b % 2 = 1
ha3 : a % 4 = 3
⊢ (if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)) = J(↑a | b)

Tactic:
rcases Nat.odd_mod_four_iff.mp hb2 with hb1 | hb3

Result:
case inr.inl
a b : ℕ
ha2 : a % 2 = 1
hb2 : b % 2 = 1
ha3 : a % 4 = 3
hb1 : b % 4 = 1
⊢ (if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)) = J(↑a | b)

case inr.inr
a b : ℕ
ha2 : a % 2 = 1
hb2 : b % 2 = 1
ha3 : a % 4 = 3
hb3 : b % 4 = 3
⊢ (if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)) = J(↑a | b)

Proof state:
a b : ℕ
ha2 : a % 2 = 1
hb2 : b % 2 = 1
⊢ (if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)) = J(↑a | b)

Tactic:
rcases Nat.odd_mod_four_iff.mp ha2 with ha1 | ha3

Result:
case inl
a b : ℕ
ha2 : a % 2 = 1
hb2 : b % 2 = 1
ha1 : a % 4 = 1
⊢ (if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)) = J(↑a | b)

case inr
a b : ℕ
ha2 : a % 2 = 1
hb2 : b % 2 = 1
ha3 : a % 4 = 3
⊢ (if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)) = J(↑a | b)

Proof state:
case inl
a b : ℕ
ha2 : a % 2 = 1
hb2 : b % 2 = 1
ha1 : a % 4 = 1
⊢ (if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)) = J(↑a | b)

Tactic:
simpa [ha1] using jacobiSym.quadratic_reciprocity_one_mod_four' (Nat.odd_iff.mpr hb2) ha1

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Radical.lean
theorem natDegree_radical_le {a : k[X]} :
    (radical a).natDegree ≤ a.natDegree

Proof state:
case neg
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a : k[X]
ha : ¬a = 0
⊢ (radical a).natDegree ≤ a.natDegree

Tactic:
exact natDegree_le_of_dvd (radical_dvd_self a) ha

Result:
no goals

Proof state:
case pos
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a : k[X]
ha : a = 0
⊢ (radical a).natDegree ≤ a.natDegree

Tactic:
simp [ha]

Result:
no goals

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a : k[X]
⊢ (radical a).natDegree ≤ a.natDegree

Tactic:
by_cases ha : a = 0

Result:
case pos
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a : k[X]
ha : a = 0
⊢ (radical a).natDegree ≤ a.natDegree

case neg
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a : k[X]
ha : ¬a = 0
⊢ (radical a).natDegree ≤ a.natDegree
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_preimage_equiv_lift {β : Type v} (f : α ≃ β) (s : Set β) :
    lift.{v} #(f ⁻¹' s) = lift.{u} #s

Proof state:
α : Type u
β : Type v
f : α ≃ β
s : Set β
⊢ s ⊆ univ

Tactic:
exact fun _ _ ↦ ⟨⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α ≃ β
s : Set β
⊢ lift.{v, u} #↑(⇑f ⁻¹' s) = lift.{u, v} #↑s

Tactic:
apply mk_preimage_of_injective_of_subset_range_lift _ _ f.injective

Result:
α : Type u
β : Type v
f : α ≃ β
s : Set β
⊢ s ⊆ range ⇑f

Proof state:
α : Type u
β : Type v
f : α ≃ β
s : Set β
⊢ s ⊆ range ⇑f

Tactic:
rw [f.range_eq_univ]

Result:
α : Type u
β : Type v
f : α ≃ β
s : Set β
⊢ s ⊆ univ
-- Mathlib/RingTheory/MvPowerSeries/Inverse.lean
theorem coeff_invOfUnit [DecidableEq σ] (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (u : Rˣ) :
    coeff R n (invOfUnit φ u) =
      if n = 0 then ↑u⁻¹
      else
        -↑u⁻¹ *
          ∑ x ∈ antidiagonal n,
            if x.2 < n then coeff R x.1 φ * coeff R x.2 (invOfUnit φ u) else 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
u : Rˣ
⊢ (coeff R n) (φ.invOfUnit u) =
    if n = 0 then ↑u⁻¹
    else -↑u⁻¹ * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff R x.1) φ * (coeff R x.2) (φ.invOfUnit u) else 0

Tactic:
convert coeff_inv_aux n (↑u⁻¹) φ

Result:
no goals
-- Mathlib/Algebra/Lie/Solvable.lean
theorem derivedSeries_lt_top_of_solvable [IsSolvable L] [Nontrivial L] :
    derivedSeries R L 1 < ⊤

Proof state:
case intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsSolvable L
inst✝ : Nontrivial L
n : ℕ
hn : derivedSeries R L n = ⊥
contra : derivedSeries R L 1 = ⊤
⊢ False

Tactic:
rw [LieIdeal.derivedSeries_eq_top n contra] at hn

Result:
case intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsSolvable L
inst✝ : Nontrivial L
n : ℕ
hn : ⊤ = ⊥
contra : derivedSeries R L 1 = ⊤
⊢ False

Proof state:
case intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsSolvable L
inst✝ : Nontrivial L
n : ℕ
hn : ⊤ = ⊥
contra : derivedSeries R L 1 = ⊤
⊢ False

Tactic:
exact top_ne_bot hn

Result:
no goals

Proof state:
case intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsSolvable L
inst✝ : Nontrivial L
n : ℕ
hn : derivedSeries R L n = ⊥
⊢ derivedSeries R L 1 ≠ ⊤

Tactic:
intro contra

Result:
case intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsSolvable L
inst✝ : Nontrivial L
n : ℕ
hn : derivedSeries R L n = ⊥
contra : derivedSeries R L 1 = ⊤
⊢ False

Proof state:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsSolvable L
inst✝ : Nontrivial L
⊢ derivedSeries R L 1 < ⊤

Tactic:
obtain ⟨n, hn⟩ := IsSolvable.solvable (R := R) (L := L)

Result:
case intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsSolvable L
inst✝ : Nontrivial L
n : ℕ
hn : derivedSeries R L n = ⊥
⊢ derivedSeries R L 1 < ⊤

Proof state:
case intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsSolvable L
inst✝ : Nontrivial L
n : ℕ
hn : derivedSeries R L n = ⊥
⊢ derivedSeries R L 1 < ⊤

Tactic:
rw [lt_top_iff_ne_top]

Result:
case intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsSolvable L
inst✝ : Nontrivial L
n : ℕ
hn : derivedSeries R L n = ⊥
⊢ derivedSeries R L 1 ≠ ⊤
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
/-- If the pushout comparison map for `G` at `(f,g)` is an isomorphism, then `G` preserves the
pushout of `(f,g)`. -/
lemma PreservesPushout.of_iso_comparison [i : IsIso (pushoutComparison G f g)] :
    PreservesColimit (span f g) G

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
i : IsIso (pushoutComparison G f g)
⊢ IsColimit (PushoutCocone.mk (G.map (pushout.inl f g)) (G.map (pushout.inr f g)) ⋯)

Tactic:
exact @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (span (G.map f) (G.map g))) i

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
i : IsIso (pushoutComparison G f g)
⊢ PreservesColimit (span f g) G

Tactic:
apply preservesColimit_of_preserves_colimit_cocone (pushoutIsPushout f g)

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
i : IsIso (pushoutComparison G f g)
⊢ IsColimit (G.mapCocone (PushoutCocone.mk (pushout.inl f g) (pushout.inr f g) ⋯))

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
i : IsIso (pushoutComparison G f g)
⊢ IsColimit (G.mapCocone (PushoutCocone.mk (pushout.inl f g) (pushout.inr f g) ⋯))

Tactic:
apply (isColimitMapCoconePushoutCoconeEquiv _ _).symm _

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
i : IsIso (pushoutComparison G f g)
⊢ IsColimit (PushoutCocone.mk (G.map (pushout.inl f g)) (G.map (pushout.inr f g)) ⋯)
-- Mathlib/Algebra/Group/Units/Defs.lean
theorem mul_divp_cancel (a : α) (u : αˣ) : a * u /ₚ u = a :=
  (mul_assoc _ _ _).trans <| by rw [Units.mul_inv, mul_one]

Proof state:
α : Type u
inst✝ : Monoid α
a : α
u : αˣ
⊢ a * (↑u * ↑u⁻¹) = a

Tactic:
rw [Units.mul_inv, mul_one]

Result:
no goals
-- Mathlib/Data/Int/ModEq.lean
theorem modEq_zero_iff : a ≡ b [ZMOD 0] ↔ a = b

Proof state:
a b : ℤ
⊢ a ≡ b [ZMOD 0] ↔ a = b

Tactic:
rw [ModEq, emod_zero, emod_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem add_one_pos (i : Fin (n + 1)) (h : i < Fin.last n) : (0 : Fin (n + 1)) < i + 1

Proof state:
n✝ n : Nat
i : Fin (n + 1 + 1)
h✝ : ↑i < n + 1
h : ↑i + 1 < n + 1 + 1
⊢ 0 < ↑i + 1

Tactic:
exact Nat.zero_lt_succ _

Result:
no goals

Proof state:
n✝ n : Nat
i : Fin (n + 1 + 1)
h✝ : ↑i < n + 1
h : ↑i + ?m.19042 < n + 1 + ?m.19042
⊢ 0 < i + 1

n✝ n : Nat
i : Fin (n + 1 + 1)
h : ↑i < n + 1
⊢ Nat

Tactic:
rw [Fin.lt_def, val_add, val_zero, val_one, Nat.mod_eq_of_lt h]

Result:
n✝ n : Nat
i : Fin (n + 1 + 1)
h✝ : ↑i < n + 1
h : ↑i + 1 < n + 1 + 1
⊢ 0 < ↑i + 1

Proof state:
n : Nat
i : Fin (0 + 1)
h : i < last 0
⊢ 0 < i + 1

Tactic:
cases h

Result:
no goals

Proof state:
n✝ n : Nat
i : Fin (n + 1 + 1)
h : i < last (n + 1)
⊢ 0 < i + 1

Tactic:
rw [Fin.lt_def, val_last, ← Nat.add_lt_add_iff_right] at h

Result:
n✝ n : Nat
i : Fin (n + 1 + 1)
h✝ : ↑i < n + 1
h : ↑i + ?m.19042 < n + 1 + ?m.19042
⊢ 0 < i + 1

n✝ n : Nat
i : Fin (n + 1 + 1)
h : ↑i < n + 1
⊢ Nat

Proof state:
n : Nat
i : Fin (n + 1)
h : i < last n
⊢ 0 < i + 1

Tactic:
match n with
| 0 => cases h
| n+1 =>
  rw [Fin.lt_def, val_last, ← Nat.add_lt_add_iff_right] at h
  rw [Fin.lt_def, val_add, val_zero, val_one, Nat.mod_eq_of_lt h]
  exact Nat.zero_lt_succ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem ite_eq_false_distrib (p : Prop) [h : Decidable p] (t f : Bool) :
    (ite p t f = false) = ite p (t = false) (f = false)

Proof state:
case isTrue
p✝ : Prop
t f : Bool
p : p✝
⊢ ((if p✝ then t else f) = false) = if p✝ then t = false else f = false

Tactic:
simp [p]

Result:
no goals

Proof state:
p : Prop
h : Decidable p
t f : Bool
⊢ ((if p then t else f) = false) = if p then t = false else f = false

Tactic:
cases h with | _ p => simp [p]

Result:
no goals
-- Mathlib/MeasureTheory/Function/Egorov.lean
theorem iUnionNotConvergentSeq_subset (hε : 0 < ε) (hf : ∀ n, StronglyMeasurable (f n))
    (hg : StronglyMeasurable g) (hsm : MeasurableSet s) (hs : μ s ≠ ∞)
    (hfg : ∀ᵐ x ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))) :
    iUnionNotConvergentSeq hε hf hg hsm hs hfg ⊆ s

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ iUnionNotConvergentSeq hε hf hg hsm hs hfg ⊆ s

Tactic:
rw [iUnionNotConvergentSeq, ← Set.inter_iUnion]

Result:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ s ∩ ⋃ i, notConvergentSeq f g i (notConvergentSeqLTIndex ⋯ hf hg hsm hs hfg i) ⊆ s

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ s ∩ ⋃ i, notConvergentSeq f g i (notConvergentSeqLTIndex ⋯ hf hg hsm hs hfg i) ⊆ s

Tactic:
exact Set.inter_subset_left

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean
theorem mono_of_mono_of_mono_of_mono (hR₁ : R₁.Exact)
    (hR₂' : Mono (R₂.map' 0 1))
    (h₀ : Mono (app' φ 0))
    (h₁ : Mono (app' φ 2)) :
    Mono (app' φ 1)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂' : Mono (R₂.map' 0 1 ⋯ ⋯)
h₀ : Mono (app' φ 0 ⋯)
h₁ : Mono (app' φ 2 ⋯)
ψ : mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₃ (𝟙 ((mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).obj' 0 ⋯)) (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯
⊢ Mono (app' φ 1 ⋯)

Tactic:
refine mono_of_epi_of_mono_of_mono' ψ (by simp)
  (hR₁.exact 0).exact_toComposableArrows
  (exact₂_mk _ (by simp) ?_) (by dsimp [ψ]; infer_instance) h₀ h₁

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂' : Mono (R₂.map' 0 1 ⋯ ⋯)
h₀ : Mono (app' φ 0 ⋯)
h₁ : Mono (app' φ 2 ⋯)
ψ : mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₃ (𝟙 ((mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).obj' 0 ⋯)) (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯
⊢ (ShortComplex.mk
      ((mk₂ ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 0 1 ⋯ ⋯)
            ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 ⋯ ⋯)).map'
        0 1 ⋯ ⋯)
      ((mk₂ ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 0 1 ⋯ ⋯)
            ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 ⋯ ⋯)).map'
        1 2 ⋯ ⋯)
      ⋯).Exact
-- Mathlib/LinearAlgebra/Finsupp/LSum.lean
theorem lcongr_symm {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) :
    (lcongr e₁ e₂).symm = lcongr e₁.symm e₂.symm

Proof state:
M : Type u_2
N : Type u_3
R : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_7
κ : Type u_8
e₁ : ι ≃ κ
e₂ : M ≃ₗ[R] N
⊢ (lcongr e₁ e₂).symm = lcongr e₁.symm e₂.symm

Tactic:
ext

Result:
case h.h
M : Type u_2
N : Type u_3
R : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_7
κ : Type u_8
e₁ : ι ≃ κ
e₂ : M ≃ₗ[R] N
x✝ : κ →₀ N
a✝ : ι
⊢ ((lcongr e₁ e₂).symm x✝) a✝ = ((lcongr e₁.symm e₂.symm) x✝) a✝

Proof state:
case h.h
M : Type u_2
N : Type u_3
R : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_7
κ : Type u_8
e₁ : ι ≃ κ
e₂ : M ≃ₗ[R] N
x✝ : κ →₀ N
a✝ : ι
⊢ ((lcongr e₁ e₂).symm x✝) a✝ = ((lcongr e₁.symm e₂.symm) x✝) a✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/List/Infix.lean
theorem inits_eq_tails : ∀ l : List α, l.inits = (reverse <| map reverse <| tails <| reverse l)
  | [] => by simp
  | a :: l => by simp [inits_eq_tails l, map_inj_left, ← map_reverse]

Proof state:
α : Type u_1
a : α
l : List α
⊢ (a :: l).inits = (map reverse (a :: l).reverse.tails).reverse

Tactic:
simp [inits_eq_tails l, map_inj_left, ← map_reverse]

Result:
no goals

Proof state:
α : Type u_1
⊢ [].inits = (map reverse [].reverse.tails).reverse

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem discr_prime_pow_eq_unit_mul_pow' [IsCyclotomicExtension {p ^ k} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) :
    ∃ (u : ℤˣ) (n : ℕ), discr ℚ (hζ.subOnePowerBasis ℚ).basis = u * p ^ n

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ ∃ u n, Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑p ^ n

Tactic:
rw [hζ.discr_zeta_eq_discr_zeta_sub_one.symm]

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ ∃ u n, Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = ↑↑u * ↑↑p ^ n

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ ∃ u n, Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = ↑↑u * ↑↑p ^ n

Tactic:
exact discr_prime_pow_eq_unit_mul_pow hζ (cyclotomic.irreducible_rat (p ^ k).pos)

Result:
no goals