harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem count_pow [Nontrivial α] {a : Associates α} (ha : a ≠ 0)
    {p : Associates α} (hp : Irreducible p) (k : ℕ) :
    count p (a ^ k).factors = k * count p a.factors

Proof state:
case succ
α : Type u_1
inst✝⁴ : CancelCommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
n : ℕ
h : p.count (a ^ n).factors = n * p.count a.factors
⊢ p.count (a ^ (n + 1)).factors = (n + 1) * p.count a.factors

Tactic:
rw [pow_succ', count_mul ha (pow_ne_zero _ ha) hp, h]

Result:
case succ
α : Type u_1
inst✝⁴ : CancelCommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
n : ℕ
h : p.count (a ^ n).factors = n * p.count a.factors
⊢ p.count a.factors + n * p.count a.factors = (n + 1) * p.count a.factors

Proof state:
case succ
α : Type u_1
inst✝⁴ : CancelCommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
n : ℕ
h : p.count (a ^ n).factors = n * p.count a.factors
⊢ p.count a.factors + n * p.count a.factors = (n + 1) * p.count a.factors

Tactic:
ring

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : CancelCommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
k : ℕ
⊢ p.count (a ^ k).factors = k * p.count a.factors

Tactic:
induction' k with n h

Result:
case zero
α : Type u_1
inst✝⁴ : CancelCommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
⊢ p.count (a ^ 0).factors = 0 * p.count a.factors

case succ
α : Type u_1
inst✝⁴ : CancelCommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
n : ℕ
h : p.count (a ^ n).factors = n * p.count a.factors
⊢ p.count (a ^ (n + 1)).factors = (n + 1) * p.count a.factors

Proof state:
case zero
α : Type u_1
inst✝⁴ : CancelCommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
⊢ p.count (a ^ 0).factors = 0 * p.count a.factors

Tactic:
rw [pow_zero, factors_one, zero_mul, count_zero hp]

Result:
no goals
-- Mathlib/GroupTheory/CommutingProbability.lean
theorem commProb_def' : commProb G = Nat.card (ConjClasses G) / Nat.card G

Proof state:
G : Type u_2
inst✝ : Group G
⊢ commProb G = ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)

Tactic:
rw [commProb, card_comm_eq_card_conjClasses_mul_card, Nat.cast_mul, sq]

Result:
G : Type u_2
inst✝ : Group G
⊢ ↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / (↑(Nat.card G) * ↑(Nat.card G)) =
    ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)

Proof state:
case neg
G : Type u_2
inst✝ : Group G
h : ¬↑(Nat.card G) = 0
⊢ ↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / (↑(Nat.card G) * ↑(Nat.card G)) =
    ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)

Tactic:
exact mul_div_mul_right _ _ h

Result:
no goals

Proof state:
G : Type u_2
inst✝ : Group G
⊢ ↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / (↑(Nat.card G) * ↑(Nat.card G)) =
    ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)

Tactic:
by_cases h : (Nat.card G : ℚ) = 0

Result:
case pos
G : Type u_2
inst✝ : Group G
h : ↑(Nat.card G) = 0
⊢ ↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / (↑(Nat.card G) * ↑(Nat.card G)) =
    ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)

case neg
G : Type u_2
inst✝ : Group G
h : ¬↑(Nat.card G) = 0
⊢ ↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / (↑(Nat.card G) * ↑(Nat.card G)) =
    ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)

Proof state:
case pos
G : Type u_2
inst✝ : Group G
h : ↑(Nat.card G) = 0
⊢ ↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / (↑(Nat.card G) * ↑(Nat.card G)) =
    ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)

Tactic:
rw [h, zero_mul, div_zero, div_zero]

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
lemma isoSpec_inv_preimage_zeroLocus [IsAffine X] (s : Set Γ(X, ⊤)) :
    X.isoSpec.inv.base ⁻¹' X.zeroLocus s = PrimeSpectrum.zeroLocus s

Proof state:
X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ ⇑(hom X.isoSpec.inv.base) ⁻¹' X.zeroLocus s = PrimeSpectrum.zeroLocus s

Tactic:
rw [← toSpecΓ_preimage_zeroLocus, ← Set.preimage_comp, ← TopCat.coe_comp, ← Scheme.comp_base,
  X.isoSpec_inv_toSpecΓ]

Result:
X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ ⇑(hom (𝟙 (Spec Γ(X, ⊤))).base) ⁻¹' PrimeSpectrum.zeroLocus s = PrimeSpectrum.zeroLocus s

Proof state:
X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ ⇑(hom (𝟙 (Spec Γ(X, ⊤))).base) ⁻¹' PrimeSpectrum.zeroLocus s = PrimeSpectrum.zeroLocus s

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Boundary.lean
lemma boundaryGE_embeddingUpIntGE_iff (p : ℤ) (n : ℕ) :
    (embeddingUpIntGE p).BoundaryGE n ↔ n = 0

Proof state:
case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
⊢ n + 1 = 0

Tactic:
have := h.2 n

Result:
case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
this : ¬(up ℤ).Rel ((embeddingUpIntGE p).f n) ((embeddingUpIntGE p).f (n + 1))
⊢ n + 1 = 0

Proof state:
case mpr
p : ℤ
n : ℕ
⊢ n = 0 → (embeddingUpIntGE p).BoundaryGE n

Tactic:
rintro rfl

Result:
case mpr
p : ℤ
⊢ (embeddingUpIntGE p).BoundaryGE 0

Proof state:
case mpr.right
p : ℤ
i : ℕ
hi : p + ↑i + 1 = p + 0
⊢ False

Tactic:
omega

Result:
no goals

Proof state:
case mpr.left
p : ℤ
⊢ (up ℤ).Rel ((up ℤ).prev ((embeddingUpIntGE p).f 0)) ((embeddingUpIntGE p).f 0)

Tactic:
simp

Result:
no goals

Proof state:
case mp
p : ℤ
n : ℕ
⊢ (embeddingUpIntGE p).BoundaryGE n → n = 0

Tactic:
intro h

Result:
case mp
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE n
⊢ n = 0

Proof state:
case mp.zero
p : ℤ
h : (embeddingUpIntGE p).BoundaryGE 0
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case mp
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE n
⊢ n = 0

Tactic:
obtain _|n := n

Result:
case mp.zero
p : ℤ
h : (embeddingUpIntGE p).BoundaryGE 0
⊢ 0 = 0

case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
⊢ n + 1 = 0

Proof state:
case mpr.right
p : ℤ
⊢ ∀ (i : ℕ), ¬(up ℤ).Rel ((embeddingUpIntGE p).f i) ((embeddingUpIntGE p).f 0)

Tactic:
intro i hi

Result:
case mpr.right
p : ℤ
i : ℕ
hi : (up ℤ).Rel ((embeddingUpIntGE p).f i) ((embeddingUpIntGE p).f 0)
⊢ False

Proof state:
case mpr.right
p : ℤ
i : ℕ
hi : (up ℤ).Rel ((embeddingUpIntGE p).f i) ((embeddingUpIntGE p).f 0)
⊢ False

Tactic:
dsimp at hi

Result:
case mpr.right
p : ℤ
i : ℕ
hi : p + ↑i + 1 = p + 0
⊢ False

Proof state:
case mpr
p : ℤ
⊢ (embeddingUpIntGE p).BoundaryGE 0

Tactic:
constructor

Result:
case mpr.left
p : ℤ
⊢ (up ℤ).Rel ((up ℤ).prev ((embeddingUpIntGE p).f 0)) ((embeddingUpIntGE p).f 0)

case mpr.right
p : ℤ
⊢ ∀ (i : ℕ), ¬(up ℤ).Rel ((embeddingUpIntGE p).f i) ((embeddingUpIntGE p).f 0)

Proof state:
p : ℤ
n : ℕ
⊢ (embeddingUpIntGE p).BoundaryGE n ↔ n = 0

Tactic:
constructor

Result:
case mp
p : ℤ
n : ℕ
⊢ (embeddingUpIntGE p).BoundaryGE n → n = 0

case mpr
p : ℤ
n : ℕ
⊢ n = 0 → (embeddingUpIntGE p).BoundaryGE n

Proof state:
case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
this : ¬(up ℤ).Rel ((embeddingUpIntGE p).f n) ((embeddingUpIntGE p).f (n + 1))
⊢ n + 1 = 0

Tactic:
dsimp at this

Result:
case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
this : ¬p + ↑n + 1 = p + ↑(n + 1)
⊢ n + 1 = 0

Proof state:
case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
this : ¬p + ↑n + 1 = p + ↑(n + 1)
⊢ n + 1 = 0

Tactic:
omega

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Opposite/Basic.lean
lemma opShiftFunctorEquivalence_unitIso_hom_app_eq (X : Cᵒᵖ) (m n p : ℤ) (h : m + n = p) :
    (opShiftFunctorEquivalence C p).unitIso.hom.app X =
      (opShiftFunctorEquivalence C n).unitIso.hom.app X ≫
      (((opShiftFunctorEquivalence C m).unitIso.hom.app (X⟦n⟧)).unop⟦n⟧').op ≫
      ((shiftFunctorAdd' C m n p h).hom.app _).op ≫
      (((shiftFunctorAdd' Cᵒᵖ n m p (by omega)).inv.app X).unop⟦p⟧').op

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctorCompIsoId C (-p) p ⋯).hom.app (Opposite.unop X)).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map
            ((shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
        ((shiftFunctorAdd' C m n p h).hom.app
              (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctor C p).map
              ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X) ≫
                𝟙 ((shiftFunctor C (-m)).obj ((shiftFunctor C (-n)).obj (Opposite.unop X))))).op

Tactic:
rw [comp_id, shiftFunctorCompIsoId_add'_hom_app _ _ _ _ _ _
  (neg_add_cancel m) (neg_add_cancel n) (neg_add_cancel p) h]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctor C p).map ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X)) ≫
        (shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C (-m)).obj ((shiftFunctor C (-n)).obj (Opposite.unop X))) ≫
          (shiftFunctor C n).map
              ((shiftFunctorCompIsoId C (-m) m ⋯).hom.app ((shiftFunctor C (-n)).obj (Opposite.unop X))) ≫
            (shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map
            ((shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
        ((shiftFunctorAdd' C m n p h).hom.app
              (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctor C p).map ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X))).op
-- Mathlib/GroupTheory/Torsion.lean
theorem torsion.isTorsion : IsTorsion <| torsion G := fun ⟨x, n, npos, hn⟩ =>
  ⟨n, npos,
    Subtype.ext <| by
      dsimp
      rw [mul_left_iterate]
      change _ * 1 = 1
      rw [_root_.mul_one, SubmonoidClass.coe_pow, Subtype.coe_mk,
        (isPeriodicPt_mul_iff_pow_eq_one _).mp hn]⟩

Proof state:
G : Type u_1
inst✝ : CommMonoid G
x✝ : ↥(torsion G)
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt (fun x_1 => x * x_1) n 1
⊢ ↑((fun x_1 => ⟨x, ⋯⟩ * x_1)^[n] 1) = ↑1

Tactic:
dsimp

Result:
G : Type u_1
inst✝ : CommMonoid G
x✝ : ↥(torsion G)
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt (fun x_1 => x * x_1) n 1
⊢ ↑((fun x_1 => ⟨x, ⋯⟩ * x_1)^[n] 1) = 1

Proof state:
G : Type u_1
inst✝ : CommMonoid G
x✝ : ↥(torsion G)
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt (fun x_1 => x * x_1) n 1
⊢ ↑((fun x_1 => ⟨x, ⋯⟩ * x_1)^[n] 1) = 1

Tactic:
rw [mul_left_iterate]

Result:
G : Type u_1
inst✝ : CommMonoid G
x✝ : ↥(torsion G)
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt (fun x_1 => x * x_1) n 1
⊢ ↑((fun x_1 => ⟨x, ⋯⟩ ^ n * x_1) 1) = 1

Proof state:
G : Type u_1
inst✝ : CommMonoid G
x✝ : ↥(torsion G)
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt (fun x_1 => x * x_1) n 1
⊢ ↑(⟨x, ⋯⟩ ^ n) * 1 = 1

Tactic:
rw [_root_.mul_one, SubmonoidClass.coe_pow, Subtype.coe_mk,
  (isPeriodicPt_mul_iff_pow_eq_one _).mp hn]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : CommMonoid G
x✝ : ↥(torsion G)
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt (fun x_1 => x * x_1) n 1
⊢ ↑((fun x_1 => ⟨x, ⋯⟩ ^ n * x_1) 1) = 1

Tactic:
change _ * 1 = 1

Result:
G : Type u_1
inst✝ : CommMonoid G
x✝ : ↥(torsion G)
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt (fun x_1 => x * x_1) n 1
⊢ ↑(⟨x, ⋯⟩ ^ n) * 1 = 1
-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem uniqueDiffOn_Icc {a b : ℝ} (hab : a < b) : UniqueDiffOn ℝ (Icc a b) :=
  uniqueDiffOn_convex (convex_Icc a b) <| by simp only [interior_Icc, nonempty_Ioo, hab]

Proof state:
a b : ℝ
hab : a < b
⊢ (interior (Icc a b)).Nonempty

Tactic:
simp only [interior_Icc, nonempty_Ioo, hab]

Result:
no goals
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem zero_eq [Nontrivial A] : σ (0 : A) = {0}

Proof state:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ {0}ᶜ ⊆ resolventSet 𝕜 0

Tactic:
intro k hk

Result:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
hk : k ∈ {0}ᶜ
⊢ k ∈ resolventSet 𝕜 0

Proof state:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
hk : k ≠ 0
⊢ k ∈ resolventSet 𝕜 0

Tactic:
have : IsUnit (Units.mk0 k hk • (1 : A)) := IsUnit.smul (Units.mk0 k hk) isUnit_one

Result:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
hk : k ≠ 0
this : IsUnit (Units.mk0 k hk • 1)
⊢ k ∈ resolventSet 𝕜 0

Proof state:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ {0} ⊆ σ 0

Tactic:
simp [Algebra.algebraMap_eq_smul_one, mem_iff]

Result:
no goals

Proof state:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
hk : k ≠ 0
this : IsUnit (Units.mk0 k hk • 1)
⊢ k ∈ resolventSet 𝕜 0

Tactic:
simpa [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one]

Result:
no goals

Proof state:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ σ 0 = {0}

Tactic:
refine Set.Subset.antisymm ?_ (by simp [Algebra.algebraMap_eq_smul_one, mem_iff])

Result:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ σ 0 ⊆ {0}

Proof state:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
hk : k ∈ {0}ᶜ
⊢ k ∈ resolventSet 𝕜 0

Tactic:
rw [Set.mem_compl_singleton_iff] at hk

Result:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
hk : k ≠ 0
⊢ k ∈ resolventSet 𝕜 0

Proof state:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ σ 0 ⊆ {0}

Tactic:
rw [spectrum, Set.compl_subset_comm]

Result:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ {0}ᶜ ⊆ resolventSet 𝕜 0
-- Mathlib/Data/List/Basic.lean
lemma cons_sublist_cons' {a b : α} : a :: l₁ <+ b :: l₂ ↔ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂

Proof state:
case mp.cons
α : Type u
l₁ l₂ : List α
a b : α
a✝ : a :: l₁ <+ l₂
⊢ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂

Tactic:
exact Or.inl ‹_›

Result:
no goals

Proof state:
α : Type u
l₁ l₂ : List α
a b : α
⊢ a :: l₁ <+ b :: l₂ ↔ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂

Tactic:
constructor

Result:
case mp
α : Type u
l₁ l₂ : List α
a b : α
⊢ a :: l₁ <+ b :: l₂ → a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂

case mpr
α : Type u
l₁ l₂ : List α
a b : α
⊢ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂ → a :: l₁ <+ b :: l₂

Proof state:
case mp
α : Type u
l₁ l₂ : List α
a b : α
⊢ a :: l₁ <+ b :: l₂ → a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂

Tactic:
rintro (_ | _)

Result:
case mp.cons
α : Type u
l₁ l₂ : List α
a b : α
a✝ : a :: l₁ <+ l₂
⊢ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂

case mp.cons₂
α : Type u
l₁ l₂ : List α
a : α
a✝ : l₁ <+ l₂
⊢ a :: l₁ <+ l₂ ∨ a = a ∧ l₁ <+ l₂

Proof state:
case mpr.inl
α : Type u
l₁ l₂ : List α
a b : α
h : a :: l₁ <+ l₂
⊢ a :: l₁ <+ b :: l₂

Tactic:
exact h.cons _

Result:
no goals

Proof state:
case mp.cons₂
α : Type u
l₁ l₂ : List α
a : α
a✝ : l₁ <+ l₂
⊢ a :: l₁ <+ l₂ ∨ a = a ∧ l₁ <+ l₂

Tactic:
exact Or.inr ⟨rfl, ‹_›⟩

Result:
no goals

Proof state:
case mpr
α : Type u
l₁ l₂ : List α
a b : α
⊢ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂ → a :: l₁ <+ b :: l₂

Tactic:
rintro (h | ⟨rfl, h⟩)

Result:
case mpr.inl
α : Type u
l₁ l₂ : List α
a b : α
h : a :: l₁ <+ l₂
⊢ a :: l₁ <+ b :: l₂

case mpr.inr.intro
α : Type u
l₁ l₂ : List α
a : α
h : l₁ <+ l₂
⊢ a :: l₁ <+ a :: l₂

Proof state:
case mpr.inr.intro
α : Type u
l₁ l₂ : List α
a : α
h : l₁ <+ l₂
⊢ a :: l₁ <+ a :: l₂

Tactic:
rwa [cons_sublist_cons]

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExactSequences.lean
lemma covariant_sequence_exact₂ {n : ℕ} (x₂ : Ext X S.X₂ n)
    (hx₂ : x₂.comp (mk₀ S.g) (add_zero n) = 0) :
    ∃ (x₁ : Ext X S.X₁ n), x₁.comp (mk₀ S.f) (add_zero n) = x₂

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
x₂ : Ext X S.X₂ n
hx₂ : x₂.comp (mk₀ S.g) ⋯ = 0
this : (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯)) ⋯).Exact
⊢ ∃ x₁, x₁.comp (mk₀ S.f) ⋯ = x₂

Tactic:
rw [ShortComplex.ab_exact_iff] at this

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
x₂ : Ext X S.X₂ n
hx₂ : x₂.comp (mk₀ S.g) ⋯ = 0
this :
  ∀
    (x₂ :
      ↑(ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯)) ⋯).X₂),
    (ConcreteCategory.hom
            (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯))
                ⋯).g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯))
                  ⋯).f)
            x₁ =
          x₂
⊢ ∃ x₁, x₁.comp (mk₀ S.f) ⋯ = x₂

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
x₂ : Ext X S.X₂ n
hx₂ : x₂.comp (mk₀ S.g) ⋯ = 0
⊢ ∃ x₁, x₁.comp (mk₀ S.f) ⋯ = x₂

Tactic:
have := covariant_sequence_exact₂' X hS n

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
x₂ : Ext X S.X₂ n
hx₂ : x₂.comp (mk₀ S.g) ⋯ = 0
this : (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯)) ⋯).Exact
⊢ ∃ x₁, x₁.comp (mk₀ S.f) ⋯ = x₂

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
x₂ : Ext X S.X₂ n
hx₂ : x₂.comp (mk₀ S.g) ⋯ = 0
this :
  ∀
    (x₂ :
      ↑(ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯)) ⋯).X₂),
    (ConcreteCategory.hom
            (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯))
                ⋯).g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯))
                  ⋯).f)
            x₁ =
          x₂
⊢ ∃ x₁, x₁.comp (mk₀ S.f) ⋯ = x₂

Tactic:
exact this x₂ hx₂

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem toList_eraseP (p) (l : AssocList α β) :
    (eraseP p l).toList = l.toList.eraseP fun (a, b) => p a b

Proof state:
case cons
α : Type u_1
β : Type u_2
p : α → β → Bool
key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ :
  (eraseP p tail✝).toList =
    List.eraseP
      (fun x =>
        match x with
        | (a, b) => p a b)
      tail✝.toList
⊢ (match p key✝ value✝ with
      | true => tail✝
      | false => cons key✝ value✝ (eraseP p tail✝)).toList =
    match p key✝ value✝ with
    | true => tail✝.toList
    | false => (key✝, value✝) :: List.eraseP (fun x => p x.fst x.snd) tail✝.toList

Tactic:
split <;> simp [*]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → β → Bool
l : AssocList α β
⊢ (eraseP p l).toList =
    List.eraseP
      (fun x =>
        match x with
        | (a, b) => p a b)
      l.toList

Tactic:
induction l <;> simp [List.eraseP, cond]

Result:
case cons
α : Type u_1
β : Type u_2
p : α → β → Bool
key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ :
  (eraseP p tail✝).toList =
    List.eraseP
      (fun x =>
        match x with
        | (a, b) => p a b)
      tail✝.toList
⊢ (match p key✝ value✝ with
      | true => tail✝
      | false => cons key✝ value✝ (eraseP p tail✝)).toList =
    match p key✝ value✝ with
    | true => tail✝.toList
    | false => (key✝, value✝) :: List.eraseP (fun x => p x.fst x.snd) tail✝.toList
-- Mathlib/Data/Finset/Image.lean
theorem map_erase [DecidableEq α] (f : α ↪ β) (s : Finset α) (a : α) :
    (s.erase a).map f = (s.map f).erase (f a)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α ↪ β
s : Finset α
a : α
⊢ map f (s.erase a) = (map f s).erase (f a)

Tactic:
simp_rw [map_eq_image]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α ↪ β
s : Finset α
a : α
⊢ image (⇑f) (s.erase a) = (image (⇑f) s).erase (f a)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α ↪ β
s : Finset α
a : α
⊢ image (⇑f) (s.erase a) = (image (⇑f) s).erase (f a)

Tactic:
exact s.image_erase f.2 a

Result:
no goals
-- Mathlib/Algebra/Ring/Ext.lean
theorem toNonUnitalNonAssocSemiring_injective :
    Function.Injective (@toNonUnitalNonAssocSemiring R)

Proof state:
R : Type u
a₁✝ a₂✝ : NonAssocSemiring R
a✝ : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
⊢ a₁✝ = a₂✝

Tactic:
ext <;> congr

Result:
no goals

Proof state:
R : Type u
⊢ Function.Injective (@toNonUnitalNonAssocSemiring R)

Tactic:
intro _ _ _

Result:
R : Type u
a₁✝ a₂✝ : NonAssocSemiring R
a✝ : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
⊢ a₁✝ = a₂✝
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem discreteTopology_of_isOpen_singleton_one (h : IsOpen ({1} : Set G)) :
    DiscreteTopology G

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
⊢ ∀ (a : G), IsOpen {a}

Tactic:
intro g

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
g : G
⊢ IsOpen {g}

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
g : G
this : {g} = (fun x => g⁻¹ * x) ⁻¹' {1}
⊢ IsOpen {g}

Tactic:
rw [this]

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
g : G
this : {g} = (fun x => g⁻¹ * x) ⁻¹' {1}
⊢ IsOpen ((fun x => g⁻¹ * x) ⁻¹' {1})

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
⊢ DiscreteTopology G

Tactic:
rw [← singletons_open_iff_discrete]

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
⊢ ∀ (a : G), IsOpen {a}

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
g : G
⊢ {g} = (fun x => g⁻¹ * x) ⁻¹' {1}

Tactic:
simp only [mul_one, Set.preimage_mul_left_singleton, eq_self_iff_true, inv_inv,
  Set.singleton_eq_singleton_iff]

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
g : G
this : {g} = (fun x => g⁻¹ * x) ⁻¹' {1}
⊢ IsOpen ((fun x => g⁻¹ * x) ⁻¹' {1})

Tactic:
exact (continuous_mul_left g⁻¹).isOpen_preimage _ h

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem lt_sq_of_sqrt_lt (h : √x < y) : x < y ^ 2

Proof state:
x y : ℝ
h : √x < y
hy : 0 < y
⊢ x < y ^ 2

Tactic:
rwa [← sqrt_lt_sqrt_iff_of_pos (sq_pos_of_pos hy), sqrt_sq hy.le]

Result:
no goals

Proof state:
x y : ℝ
h : √x < y
⊢ x < y ^ 2

Tactic:
have hy := x.sqrt_nonneg.trans_lt h

Result:
x y : ℝ
h : √x < y
hy : 0 < y
⊢ x < y ^ 2