harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
private lemma zeta_mul_mu' : (zeta 𝕜 * mu' 𝕜 : IncidenceAlgebra 𝕜 α) = 1

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
a✝ : a ≤ b
⊢ (zeta 𝕜 * IncidenceAlgebra.mu' 𝕜) a b = ∑ x ∈ Icc a b, (IncidenceAlgebra.mu' 𝕜) x b

Tactic:
rw [mul_apply]

Result:
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
a✝ : a ≤ b
⊢ ∑ x ∈ Icc a b, (zeta 𝕜) a x * (IncidenceAlgebra.mu' 𝕜) x b = ∑ x ∈ Icc a b, (IncidenceAlgebra.mu' 𝕜) x b

Proof state:
case a
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
a✝ : a ≤ b
x : α
hx : x ∈ Icc a b
⊢ (zeta 𝕜) a x * (IncidenceAlgebra.mu' 𝕜) x b = (IncidenceAlgebra.mu' 𝕜) x b

Tactic:
simp [(mem_Icc.1 hx).1]

Result:
no goals

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
⊢ zeta 𝕜 * IncidenceAlgebra.mu' 𝕜 = 1

Tactic:
ext a b

Result:
case h
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
a✝ : a ≤ b
⊢ (zeta 𝕜 * IncidenceAlgebra.mu' 𝕜) a b = 1 a b

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
a✝ : a ≤ b
⊢ ∑ x ∈ Icc a b, (zeta 𝕜) a x * (IncidenceAlgebra.mu' 𝕜) x b = ∑ x ∈ Icc a b, (IncidenceAlgebra.mu' 𝕜) x b

Tactic:
congr! with x hx

Result:
case a
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
a✝ : a ≤ b
x : α
hx : x ∈ Icc a b
⊢ (zeta 𝕜) a x * (IncidenceAlgebra.mu' 𝕜) x b = (IncidenceAlgebra.mu' 𝕜) x b

Proof state:
case h
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
a✝ : a ≤ b
⊢ (zeta 𝕜 * IncidenceAlgebra.mu' 𝕜) a b = 1 a b

Tactic:
calc
  _ = ∑ x ∈ Icc a b, mu' 𝕜 x b := by rw [mul_apply]; congr! with x hx; simp [(mem_Icc.1 hx).1]
  _ = (1 : IncidenceAlgebra 𝕜 α) a b := sum_Icc_mu'_left ..

Result:
no goals
-- Mathlib/Algebra/Group/UniqueProds/Basic.lean
theorem set_subsingleton (h : UniqueMul A B a0 b0) :
    Set.Subsingleton { ab : G × G | ab.1 ∈ A ∧ ab.2 ∈ B ∧ ab.1 * ab.2 = a0 * b0 }

Proof state:
case mk.mk
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x1 y1 : G
hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = a0 * b0
x2 y2 : G
hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = a0 * b0
⊢ (x1, y1) = (x2, y2)

Tactic:
rcases h hx.1 hx.2.1 hx.2.2 with ⟨rfl, rfl⟩

Result:
case mk.mk.intro
G : Type u_1
inst✝ : Mul G
A B : Finset G
x1 y1 x2 y2 : G
h : UniqueMul A B x1 y1
hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = x1 * y1
hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = x1 * y1
⊢ (x1, y1) = (x2, y2)

Proof state:
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
⊢ {ab | ab.1 ∈ A ∧ ab.2 ∈ B ∧ ab.1 * ab.2 = a0 * b0}.Subsingleton

Tactic:
rintro ⟨x1, y1⟩ (hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = a0 * b0) ⟨x2, y2⟩
  (hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = a0 * b0)

Result:
case mk.mk
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x1 y1 : G
hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = a0 * b0
x2 y2 : G
hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = a0 * b0
⊢ (x1, y1) = (x2, y2)

Proof state:
case mk.mk.intro.intro
G : Type u_1
inst✝ : Mul G
A B : Finset G
x2 y2 : G
h : UniqueMul A B x2 y2
hx hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = x2 * y2
⊢ (x2, y2) = (x2, y2)

Tactic:
rfl

Result:
no goals

Proof state:
case mk.mk.intro
G : Type u_1
inst✝ : Mul G
A B : Finset G
x1 y1 x2 y2 : G
h : UniqueMul A B x1 y1
hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = x1 * y1
hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = x1 * y1
⊢ (x1, y1) = (x2, y2)

Tactic:
rcases h hy.1 hy.2.1 hy.2.2 with ⟨rfl, rfl⟩

Result:
case mk.mk.intro.intro
G : Type u_1
inst✝ : Mul G
A B : Finset G
x2 y2 : G
h : UniqueMul A B x2 y2
hx hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = x2 * y2
⊢ (x2, y2) = (x2, y2)
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem scanl_eq_scanlTR : @scanl = @scanlTR

Proof state:
case h.h.h.h
α : Type u_2
f : Type u_1
n : α → f → α
l : α
⊢ scanl n l = scanlTR n l

Tactic:
simp (config := { unfoldPartialApp := true }) [scanlTR, scanlTR_go_eq]

Result:
no goals

Proof state:
⊢ @scanl = @scanlTR

Tactic:
funext α f n l

Result:
case h.h.h.h
α : Type u_2
f : Type u_1
n : α → f → α
l : α
⊢ scanl n l = scanlTR n l
-- Mathlib/CategoryTheory/Shift/Basic.lean
theorem shiftZero' : f⟦(0 : A)⟧' = (shiftZero A X).hom ≫ f ≫ (shiftZero A Y).inv

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
⊢ (shiftFunctor C 0).map f = (shiftZero A X).hom ≫ f ≫ (shiftZero A Y).inv

Tactic:
symm

Result:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
⊢ (shiftZero A X).hom ≫ f ≫ (shiftZero A Y).inv = (shiftFunctor C 0).map f

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
⊢ (shiftFunctorZero C A).hom.app X ≫ f ≫ (shiftFunctorZero C A).inv.app Y = (shiftFunctor C 0).map f

Tactic:
apply NatIso.naturality_2

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
⊢ (shiftZero A X).hom ≫ f ≫ (shiftZero A Y).inv = (shiftFunctor C 0).map f

Tactic:
rw [NatIso.app_inv, NatIso.app_hom]

Result:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
⊢ (shiftFunctorZero C A).hom.app X ≫ f ≫ (shiftFunctorZero C A).inv.app Y = (shiftFunctor C 0).map f
-- Mathlib/Analysis/Convex/Basic.lean
theorem Convex.vadd (hs : Convex 𝕜 s) (z : E) : Convex 𝕜 (z +ᵥ s)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z : E
⊢ Convex 𝕜 (z +ᵥ s)

Tactic:
simp_rw [← image_vadd, vadd_eq_add, ← singleton_add]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z : E
⊢ Convex 𝕜 ({z} + s)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z : E
⊢ Convex 𝕜 ({z} + s)

Tactic:
exact (convex_singleton _).add hs

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem sup_eq_lsub_iff_lt_sup {ι : Type u} (f : ι → Ordinal.{max u v}) :
    sup.{_, v} f = lsub.{_, v} f ↔ ∀ i, f i < sup.{_, v} f :=
  ⟨fun h i => by
    rw [h]
    apply lt_lsub, fun h => le_antisymm (sup_le_lsub f) (lsub_le h)⟩

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
h : sup f = lsub f
i : ι
⊢ f i < sup f

Tactic:
rw [h]

Result:
ι : Type u
f : ι → Ordinal.{max u v}
h : sup f = lsub f
i : ι
⊢ f i < lsub f

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
h : sup f = lsub f
i : ι
⊢ f i < lsub f

Tactic:
apply lt_lsub

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
lemma evaluation_coevaluation'' :
    η_ X Y ▷ X ⊗≫ X ◁ ε_ X Y = ⊗𝟙.hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : ExactPairing X Y
⊢ η_ X Y ▷ X ⊗≫ X ◁ ε_ X Y = ⊗𝟙.hom

Tactic:
convert evaluation_coevaluation X Y <;> simp [monoidalComp]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
theorem linearIndependent_subsingleton_iff [Subsingleton M] (f : ι → M) :
    LinearIndependent R f ↔ IsEmpty ι

Proof state:
case inr
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Subsingleton M
f : ι → M
i : Nonempty ι
⊢ LinearIndependent R f ↔ IsEmpty ι

Tactic:
exact iff_of_false (fun hli ↦ hli.ne_zero i.some (Subsingleton.eq_zero (f i.some))) (by simp)

Result:
no goals

Proof state:
case inl
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Subsingleton M
f : ι → M
h : IsEmpty ι
⊢ LinearIndependent R f ↔ IsEmpty ι

Tactic:
simpa

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Subsingleton M
f : ι → M
i : Nonempty ι
⊢ ¬IsEmpty ι

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Subsingleton M
f : ι → M
⊢ LinearIndependent R f ↔ IsEmpty ι

Tactic:
obtain h | i := isEmpty_or_nonempty ι

Result:
case inl
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Subsingleton M
f : ι → M
h : IsEmpty ι
⊢ LinearIndependent R f ↔ IsEmpty ι

case inr
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Subsingleton M
f : ι → M
i : Nonempty ι
⊢ LinearIndependent R f ↔ IsEmpty ι
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem take_range (m n : Nat) : take (range n) m = range (min m n)

Proof state:
m n : Nat
⊢ (range n).take m = range (min m n)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Combinatorics/Additive/Energy.lean
@[to_additive] lemma mulEnergy_comm (s t : Finset α) : Eₘ[s, t] = Eₘ[t, s]

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
s t : Finset α
⊢ #(filter ((fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) ∘ ⇑(Equiv.prodComm (α × α) (α × α)).symm)
        (map (Equiv.prodComm (α × α) (α × α)).toEmbedding ((s ×ˢ s) ×ˢ t ×ˢ t))) =
    Eₘ[t, s]

Tactic:
simp [-Finset.card_map, eq_comm, mulEnergy, mul_comm, map_eq_image, Function.comp_def]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
s t : Finset α
⊢ Eₘ[s, t] = Eₘ[t, s]

Tactic:
rw [mulEnergy, ← Finset.card_map (Equiv.prodComm _ _).toEmbedding, map_filter]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
s t : Finset α
⊢ #(filter ((fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) ∘ ⇑(Equiv.prodComm (α × α) (α × α)).symm)
        (map (Equiv.prodComm (α × α) (α × α)).toEmbedding ((s ×ˢ s) ×ˢ t ×ˢ t))) =
    Eₘ[t, s]
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem succ_mul_choose_eq : ∀ n k, succ n * choose n k = choose (succ n) (succ k) * succ k
  | 0, 0 => by decide
  | 0, k + 1 => by simp [choose]
  | n + 1, 0 => by simp [choose, mul_succ, Nat.add_comm]
  | n + 1, k + 1 => by
    rw [choose_succ_succ (succ n) (succ k), Nat.add_mul, ← succ_mul_choose_eq n, mul_succ, ←
      succ_mul_choose_eq n, Nat.add_right_comm, ← Nat.mul_add, ← choose_succ_succ, ← succ_mul]

Proof state:
n : ℕ
⊢ (n + 1).succ * (n + 1).choose 0 = (n + 1).succ.choose (succ 0) * succ 0

Tactic:
simp [choose, mul_succ, Nat.add_comm]

Result:
no goals

Proof state:
⊢ succ 0 * choose 0 0 = (succ 0).choose (succ 0) * succ 0

Tactic:
decide

Result:
no goals

Proof state:
k : ℕ
⊢ succ 0 * choose 0 (k + 1) = (succ 0).choose (k + 1).succ * (k + 1).succ

Tactic:
simp [choose]

Result:
no goals

Proof state:
n k : ℕ
⊢ (n + 1).succ * (n + 1).choose (k + 1) = (n + 1).succ.choose (k + 1).succ * (k + 1).succ

Tactic:
rw [choose_succ_succ (succ n) (succ k), Nat.add_mul, ← succ_mul_choose_eq n, mul_succ, ←
  succ_mul_choose_eq n, Nat.add_right_comm, ← Nat.mul_add, ← choose_succ_succ, ← succ_mul]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
/-- The **spectral mapping theorem** for the non-unital continuous functional calculus. -/
lemma cfcₙ_map_quasispectrum : σₙ R (cfcₙ f a) = f '' σₙ R a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
⊢ σₙ R (cfcₙ f a) = f '' σₙ R a

Tactic:
simp [cfcₙ_apply f a, cfcₙHom_map_quasispectrum (p := p)]

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplex.lean
@[reassoc (attr := simp)]
lemma XXIsoOfEq_hom_ιTotal {x₁ y₁ : I₁} (h₁ : x₁ = y₁) {x₂ y₂ : I₂} (h₂ : x₂ = y₂)
    (i₁₂ : I₁₂) (h : ComplexShape.π c₁ c₂ c₁₂ (y₁, y₂) = i₁₂) :
    (K.XXIsoOfEq _ _ _ h₁ h₂).hom ≫ K.ιTotal c₁₂ y₁ y₂ i₁₂ h =
      K.ιTotal c₁₂ x₁ x₂ i₁₂ (by rw [h₁, h₂, h])

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
x₁ : I₁
x₂ : I₂
i₁₂ : I₁₂
h : c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂
⊢ (XXIsoOfEq C c₁ c₂ K ⋯ ⋯).hom ≫ K.ιTotal c₁₂ x₁ x₂ i₁₂ h = K.ιTotal c₁₂ x₁ x₂ i₁₂ ⋯

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝⁴ : Category.{?u.67853, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
x₁ y₁ : I₁
h₁ : x₁ = y₁
x₂ y₂ : I₂
h₂ : x₂ = y₂
i₁₂ : I₁₂
h : c₁.π c₂ c₁₂ (y₁, y₂) = i₁₂
⊢ c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂

Tactic:
rw [h₁, h₂, h]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
x₁ y₁ : I₁
h₁ : x₁ = y₁
x₂ y₂ : I₂
h₂ : x₂ = y₂
i₁₂ : I₁₂
h : c₁.π c₂ c₁₂ (y₁, y₂) = i₁₂
⊢ (XXIsoOfEq C c₁ c₂ K h₁ h₂).hom ≫ K.ιTotal c₁₂ y₁ y₂ i₁₂ h = K.ιTotal c₁₂ x₁ x₂ i₁₂ ⋯

Tactic:
subst h₁ h₂

Result:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
x₁ : I₁
x₂ : I₂
i₁₂ : I₁₂
h : c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂
⊢ (XXIsoOfEq C c₁ c₂ K ⋯ ⋯).hom ≫ K.ιTotal c₁₂ x₁ x₂ i₁₂ h = K.ιTotal c₁₂ x₁ x₂ i₁₂ ⋯
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExactSequences.lean
lemma covariant_sequence_exact₁ {n₁ : ℕ} (x₁ : Ext X S.X₁ n₁)
    (hx₁ : x₁.comp (mk₀ S.f) (add_zero n₁) = 0) {n₀ : ℕ} (hn₀ : n₀ + 1 = n₁) :
    ∃ (x₃ : Ext X S.X₃ n₀), x₃.comp hS.extClass hn₀ = 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.f) ⋯ = 0
n₀ : ℕ
hn₀ : n₀ + 1 = n₁
this :
  (ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.postcomp X hn₀)) (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) ⋯).Exact
⊢ ∃ x₃, x₃.comp hS.extClass hn₀ = 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.f) ⋯ = 0
n₀ : ℕ
hn₀ : n₀ + 1 = n₁
this :
  ∀
    (x₂ :
      ↑(ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.postcomp X hn₀)) (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯))
            ⋯).X₂),
    (ConcreteCategory.hom
            (ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.postcomp X hn₀)) (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯))
                ⋯).g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              (ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.postcomp X hn₀))
                  (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) ⋯).f)
            x₁ =
          x₂
⊢ ∃ x₃, x₃.comp hS.extClass hn₀ = 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.f) ⋯ = 0
n₀ : ℕ
hn₀ : n₀ + 1 = n₁
⊢ ∃ x₃, x₃.comp hS.extClass hn₀ = x₁

Tactic:
have := covariant_sequence_exact₁' X hS n₀ n₁ hn₀

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.f) ⋯ = 0
n₀ : ℕ
hn₀ : n₀ + 1 = n₁
this :
  (ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.postcomp X hn₀)) (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) ⋯).Exact
⊢ ∃ x₃, x₃.comp hS.extClass hn₀ = 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.f) ⋯ = 0
n₀ : ℕ
hn₀ : n₀ + 1 = n₁
this :
  ∀
    (x₂ :
      ↑(ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.postcomp X hn₀)) (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯))
            ⋯).X₂),
    (ConcreteCategory.hom
            (ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.postcomp X hn₀)) (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯))
                ⋯).g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              (ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.postcomp X hn₀))
                  (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) ⋯).f)
            x₁ =
          x₂
⊢ ∃ x₃, x₃.comp hS.extClass hn₀ = x₁

Tactic:
exact this x₁ hx₁

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem abs_cos_eq_of_two_nsmul_eq {θ ψ : Angle} (h : (2 : ℕ) • θ = (2 : ℕ) • ψ) :
    |cos θ| = |cos ψ|

Proof state:
case inr
ψ : Angle
⊢ |(ψ + ↑π).cos| = |ψ.cos|

Tactic:
rw [cos_add_pi, abs_neg]

Result:
no goals

Proof state:
θ ψ : Angle
h : θ = ψ ∨ θ = ψ + ↑π
⊢ |θ.cos| = |ψ.cos|

Tactic:
rcases h with (rfl | rfl)

Result:
case inl
θ : Angle
⊢ |θ.cos| = |θ.cos|

case inr
ψ : Angle
⊢ |(ψ + ↑π).cos| = |ψ.cos|

Proof state:
θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ |θ.cos| = |ψ.cos|

Tactic:
rw [two_nsmul_eq_iff] at h

Result:
θ ψ : Angle
h : θ = ψ ∨ θ = ψ + ↑π
⊢ |θ.cos| = |ψ.cos|

Proof state:
case inl
θ : Angle
⊢ |θ.cos| = |θ.cos|

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem lift'_add (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x))
    (x y) :
    LocalizedModule.lift' S g h (x + y) =
      LocalizedModule.lift' S g h x + LocalizedModule.lift' S g h y :=
  LocalizedModule.induction_on₂
    (by
      intro a a' b b'
      rw [mk_add_mk, LocalizedModule.lift'_mk, LocalizedModule.lift'_mk, LocalizedModule.lift'_mk]
      rw [map_add, Module.End_algebraMap_isUnit_inv_apply_eq_iff, smul_add, ← map_smul,
        ← map_smul, ← map_smul]
      congr 1 <;> symm
      · rw [Module.End_algebraMap_isUnit_inv_apply_eq_iff]
        simp only [Submonoid.coe_mul, LinearMap.map_smul_of_tower]
        rw [mul_smul, Submonoid.smul_def]
      · dsimp
        rw [Module.End_algebraMap_isUnit_inv_apply_eq_iff, mul_comm, mul_smul, ← map_smul]
        rfl)
    x y

Proof state:
case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑⋯.unit⁻¹ (↑(b * b') • g a') = g (b • a')

Tactic:
dsimp

Result:
case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑⋯.unit⁻¹ ((↑b * ↑b') • g a') = g (b • a')
-- Mathlib/Tactic/NormNum/LegendreSymbol.lean
theorem jacobiSymNat.odd_even (a b c : ℕ) (r : ℤ) (ha : a % 2 = 1) (hb : b % 2 = 0) (hc : b / 2 = c)
    (hr : jacobiSymNat a c = r) : jacobiSymNat a b = r

Proof state:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
⊢ legendreSym 2 ↑1 = 1

Tactic:
decide

Result:
no goals

Proof state:
case inl
a b : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
ha' : legendreSym 2 ↑a = 1
hc : b / 2 = 0
hr : jacobiSymNat a 0 = r
⊢ jacobiSymNat a b = r

Tactic:
rw [← hr, Nat.eq_zero_of_dvd_of_div_eq_zero (Nat.dvd_of_mod_eq_zero hb) hc]

Result:
no goals

Proof state:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
⊢ jacobiSymNat a b = r

Tactic:
rcases eq_or_ne c 0 with (rfl | hc')

Result:
case inl
a b : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
ha' : legendreSym 2 ↑a = 1
hc : b / 2 = 0
hr : jacobiSymNat a 0 = r
⊢ jacobiSymNat a b = r

case inr
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
hc' : c ≠ 0
⊢ jacobiSymNat a b = r

Proof state:
case inr
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
hc' : c ≠ 0
⊢ jacobiSymNat a b = r

Tactic:
haveI : NeZero c := ⟨hc'⟩

Result:
case inr
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
hc' : c ≠ 0
this : NeZero c
⊢ jacobiSymNat a b = r

Proof state:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
⊢ legendreSym 2 ↑a = 1

Tactic:
simp only [legendreSym.mod 2 a, Int.ofNat_mod_ofNat, ha]

Result:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
⊢ legendreSym 2 ↑1 = 1

Proof state:
case inr
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
hc' : c ≠ 0
this : NeZero c
⊢ jacobiSymNat a b = r

Tactic:
rwa [← Nat.mod_add_div b 2, hb, hc, Nat.zero_add, jacobiSymNat, jacobiSym.mul_right,
  ← jacobiSym.legendreSym.to_jacobiSym, ha', one_mul]

Result:
no goals

Proof state:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
⊢ jacobiSymNat a b = r

Tactic:
have ha' : legendreSym 2 a = 1 := by
  simp only [legendreSym.mod 2 a, Int.ofNat_mod_ofNat, ha]
  decide

Result:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
⊢ jacobiSymNat a b = r
-- Mathlib/Algebra/Group/Basic.lean
theorem div_div_div_cancel_left (a b c : G) : c / a / (c / b) = b / a

Proof state:
G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ c / a / (c / b) = b / a

Tactic:
rw [← inv_div b c, div_inv_eq_mul, mul_comm, div_mul_div_cancel]

Result:
no goals
-- Mathlib/Order/Hom/Lattice.lean
theorem Disjoint.map [OrderBot α] [OrderBot β] [BotHomClass F α β] [InfHomClass F α β] {a b : α}
    (f : F) (h : Disjoint a b) : Disjoint (f a) (f b)

Proof state:
F : Type u_1
α : Type u_3
β : Type u_4
inst✝⁶ : Lattice α
inst✝⁵ : Lattice β
inst✝⁴ : FunLike F α β
inst✝³ : OrderBot α
inst✝² : OrderBot β
inst✝¹ : BotHomClass F α β
inst✝ : InfHomClass F α β
a b : α
f : F
h : Disjoint a b
⊢ Disjoint (f a) (f b)

Tactic:
rw [disjoint_iff, ← map_inf, h.eq_bot, map_bot]

Result:
no goals