harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Stream/Init.lean
theorem even_interleave (s₁ s₂ : Stream' α) : even (s₁ ⋈ s₂) = s₁ :=
  eq_of_bisim (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂))
    (fun s₁' s₁ ⟨s₂, h₁⟩ => by
      rw [h₁]
      constructor
      · rfl
      · exact ⟨tail s₂, by rw [interleave_eq, even_cons_cons, tail_cons]⟩)
    (Exists.intro s₂ rfl)

Proof state:
case left
α : Type u
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ => ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ (s₁ ⋈ s₂).even.head = s₁.head

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ => ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ (s₁ ⋈ s₂).even.head = s₁.head ∧ (fun s₁' s₁ => ∃ s₂, s₁' = (s₁ ⋈ s₂).even) (s₁ ⋈ s₂).even.tail s₁.tail

Tactic:
constructor

Result:
case left
α : Type u
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ => ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ (s₁ ⋈ s₂).even.head = s₁.head

case right
α : Type u
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ => ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ (fun s₁' s₁ => ∃ s₂, s₁' = (s₁ ⋈ s₂).even) (s₁ ⋈ s₂).even.tail s₁.tail

Proof state:
α : Type u
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ => ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ s₁'.head = s₁.head ∧ (fun s₁' s₁ => ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁'.tail s₁.tail

Tactic:
rw [h₁]

Result:
α : Type u
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ => ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ (s₁ ⋈ s₂).even.head = s₁.head ∧ (fun s₁' s₁ => ∃ s₂, s₁' = (s₁ ⋈ s₂).even) (s₁ ⋈ s₂).even.tail s₁.tail

Proof state:
case right
α : Type u
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ => ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ (fun s₁' s₁ => ∃ s₂, s₁' = (s₁ ⋈ s₂).even) (s₁ ⋈ s₂).even.tail s₁.tail

Tactic:
exact ⟨tail s₂, by rw [interleave_eq, even_cons_cons, tail_cons]⟩

Result:
no goals

Proof state:
α : Type u
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ => ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ (s₁ ⋈ s₂).even.tail = (s₁.tail ⋈ s₂.tail).even

Tactic:
rw [interleave_eq, even_cons_cons, tail_cons]

Result:
no goals
-- Mathlib/Data/Finsupp/Defs.lean
theorem support_subset_iff {s : Set α} {f : α →₀ M} :
    ↑f.support ⊆ s ↔ ∀ a ∉ s, f a = 0

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
s : Set α
f : α →₀ M
⊢ ↑f.support ⊆ s ↔ ∀ a ∉ s, f a = 0

Tactic:
simp only [Set.subset_def, mem_coe, mem_support_iff]

Result:
α : Type u_1
M : Type u_5
inst✝ : Zero M
s : Set α
f : α →₀ M
⊢ (∀ (x : α), f x ≠ 0 → x ∈ s) ↔ ∀ a ∉ s, f a = 0

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
s : Set α
f : α →₀ M
⊢ (∀ (x : α), f x ≠ 0 → x ∈ s) ↔ ∀ a ∉ s, f a = 0

Tactic:
exact forall_congr' fun a => not_imp_comm

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem map_map (f : α ↪ β) (g : β ↪ γ) (s : Finset α) : (s.map f).map g = s.map (f.trans g) :=
  eq_of_veq <| by simp only [map_val, Multiset.map_map]; rfl

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
g : β ↪ γ
s : Finset α
⊢ Multiset.map (⇑g ∘ ⇑f) s.val = Multiset.map (⇑(f.trans g)) s.val

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
g : β ↪ γ
s : Finset α
⊢ (map g (map f s)).val = (map (f.trans g) s).val

Tactic:
simp only [map_val, Multiset.map_map]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
g : β ↪ γ
s : Finset α
⊢ Multiset.map (⇑g ∘ ⇑f) s.val = Multiset.map (⇑(f.trans g)) s.val
-- Mathlib/Algebra/Star/Subalgebra.lean
lemma adjoin_le_centralizer_centralizer (s : Set A) :
    adjoin R s ≤ centralizer R (centralizer R s)

Proof state:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
⊢ adjoin R s ≤ centralizer R ↑(centralizer R s)

Tactic:
rw [← toSubalgebra_le_iff, centralizer_toSubalgebra, adjoin_toSubalgebra]

Result:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
⊢ Algebra.adjoin R (s ∪ star s) ≤ Subalgebra.centralizer R (↑(centralizer R s) ∪ star ↑(centralizer R s))

Proof state:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
⊢ Algebra.adjoin R (s ∪ star s) ≤ Subalgebra.centralizer R (↑(centralizer R s) ∪ star ↑(centralizer R s))

Tactic:
convert Algebra.adjoin_le_centralizer_centralizer R (s ∪ star s)

Result:
case h.e'_4.h.e'_6
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
⊢ ↑(centralizer R s) ∪ star ↑(centralizer R s) = ↑(Subalgebra.centralizer R (s ∪ star s))

Proof state:
case h.e'_4.h.e'_6
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
⊢ ↑(centralizer R s) ∪ ↑(centralizer R s) = ↑(Subalgebra.centralizer R (s ∪ star s))

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_4.h.e'_6
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
⊢ ↑(centralizer R s) ∪ star ↑(centralizer R s) = ↑(Subalgebra.centralizer R (s ∪ star s))

Tactic:
rw [StarMemClass.star_coe_eq]

Result:
case h.e'_4.h.e'_6
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
⊢ ↑(centralizer R s) ∪ ↑(centralizer R s) = ↑(Subalgebra.centralizer R (s ∪ star s))
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
theorem integral_condExpL2_eq_of_fin_meas_real (f : Lp 𝕜 2 μ) (hs : MeasurableSet[m] s)
    (hμs : μ s ≠ ∞) : ∫ x in s, (condExpL2 𝕜 𝕜 hm f : α → 𝕜) x ∂μ = ∫ x in s, f x ∂μ

Proof state:
α : Type u_1
𝕜 : Type u_7
inst✝ : RCLike 𝕜
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp 𝕜 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
h_eq_inner : ∫ (x : α) in s, ↑↑↑((condExpL2 𝕜 𝕜 hm) f) x ∂μ = inner (indicatorConstLp 2 ⋯ hμs 1) ↑((condExpL2 𝕜 𝕜 hm) f)
⊢ ∫ (x : α) in s, ↑↑↑((condExpL2 𝕜 𝕜 hm) f) x ∂μ = inner (indicatorConstLp 2 ⋯ hμs 1) f

Tactic:
rw [h_eq_inner, ← inner_condExpL2_left_eq_right, condExpL2_indicator_of_measurable hm hs hμs]

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_7
inst✝ : RCLike 𝕜
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp 𝕜 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ ∫ (x : α) in s, ↑↑↑((condExpL2 𝕜 𝕜 hm) f) x ∂μ = inner (indicatorConstLp 2 ⋯ hμs 1) ↑((condExpL2 𝕜 𝕜 hm) f)

Tactic:
rw [L2.inner_indicatorConstLp_one (hm s hs) hμs]

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_7
inst✝ : RCLike 𝕜
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp 𝕜 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ ∫ (x : α) in s, ↑↑↑((condExpL2 𝕜 𝕜 hm) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ

Tactic:
rw [← L2.inner_indicatorConstLp_one (𝕜 := 𝕜) (hm s hs) hμs f]

Result:
α : Type u_1
𝕜 : Type u_7
inst✝ : RCLike 𝕜
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp 𝕜 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ ∫ (x : α) in s, ↑↑↑((condExpL2 𝕜 𝕜 hm) f) x ∂μ = inner (indicatorConstLp 2 ⋯ hμs 1) f

Proof state:
α : Type u_1
𝕜 : Type u_7
inst✝ : RCLike 𝕜
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp 𝕜 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ ∫ (x : α) in s, ↑↑↑((condExpL2 𝕜 𝕜 hm) f) x ∂μ = inner (indicatorConstLp 2 ⋯ hμs 1) f

Tactic:
have h_eq_inner : ∫ x in s, (condExpL2 𝕜 𝕜 hm f : α → 𝕜) x ∂μ =
    inner (indicatorConstLp 2 (hm s hs) hμs (1 : 𝕜)) (condExpL2 𝕜 𝕜 hm f) := by
  rw [L2.inner_indicatorConstLp_one (hm s hs) hμs]

Result:
α : Type u_1
𝕜 : Type u_7
inst✝ : RCLike 𝕜
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp 𝕜 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
h_eq_inner : ∫ (x : α) in s, ↑↑↑((condExpL2 𝕜 𝕜 hm) f) x ∂μ = inner (indicatorConstLp 2 ⋯ hμs 1) ↑((condExpL2 𝕜 𝕜 hm) f)
⊢ ∫ (x : α) in s, ↑↑↑((condExpL2 𝕜 𝕜 hm) f) x ∂μ = inner (indicatorConstLp 2 ⋯ hμs 1) f
-- Mathlib/Topology/Algebra/Order/Field.lean
theorem tendsto_pow_neg_atTop {n : ℕ} (hn : n ≠ 0) :
    Tendsto (fun x : 𝕜 => x ^ (-(n : ℤ))) atTop (𝓝 0)

Proof state:
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
hn : n ≠ 0
⊢ Tendsto (fun x => x ^ (-↑n)) atTop (𝓝 0)

Tactic:
simpa only [zpow_neg, zpow_natCast] using (@tendsto_pow_atTop 𝕜 _ _ hn).inv_tendsto_atTop

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBasis.isBasis_inter_ground (hI : M.IsBasis I X) : M.IsBasis I (X ∩ M.E)

Proof state:
case h.e'_4
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ X ∩ M.E = X

Tactic:
rw [inter_eq_self_of_subset_left hI.subset_ground]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ M.IsBasis I (X ∩ M.E)

Tactic:
convert hI

Result:
case h.e'_4
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ X ∩ M.E = X
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem filter_beq (l : Array α) (a : α) : l.filter (· == a) = mkArray (count a l) a

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
toList✝ : List α
⊢ filter (fun x => x == a) { toList := toList✝ } = mkArray (count a { toList := toList✝ }) a

Tactic:
simp [List.filter_beq]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : Array α
a : α
⊢ filter (fun x => x == a) l = mkArray (count a l) a

Tactic:
cases l

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
toList✝ : List α
⊢ filter (fun x => x == a) { toList := toList✝ } = mkArray (count a { toList := toList✝ }) a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem append_left_eq_self {x y : List α} : x ++ y = y ↔ x = []

Proof state:
α : Type u_1
x y : List α
⊢ x ++ y = y ↔ x = []

Tactic:
rw [← append_left_inj (s₁ := x), nil_append]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
theorem le_inf_support_pow (degt0 : 0 ≤ degt 0) (degtm : ∀ a b, degt a + degt b ≤ degt (a + b))
    (n : ℕ) (f : R[A]) : n • f.support.inf degt ≤ (f ^ n).support.inf degt

Proof state:
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
n : ℕ
f : R[A]
⊢ n • f.support.inf degt ≤ (f ^ n).support.inf degt

Tactic:
refine OrderDual.ofDual_le_ofDual.mpr <| sup_support_pow_le (OrderDual.ofDual_le_ofDual.mp ?_)
    (fun a b => OrderDual.ofDual_le_ofDual.mp ?_) n f

Result:
case refine_1
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
n : ℕ
f : R[A]
⊢ OrderDual.ofDual (degt 0) ≤ OrderDual.ofDual 0

case refine_2
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
n : ℕ
f : R[A]
a b : A
⊢ OrderDual.ofDual (degt (a + b)) ≤ OrderDual.ofDual (degt a + degt b)

Proof state:
case refine_1
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
n : ℕ
f : R[A]
⊢ OrderDual.ofDual (degt 0) ≤ OrderDual.ofDual 0

Tactic:
exact degt0

Result:
no goals

Proof state:
case refine_2
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
n : ℕ
f : R[A]
a b : A
⊢ OrderDual.ofDual (degt (a + b)) ≤ OrderDual.ofDual (degt a + degt b)

Tactic:
exact degtm _ _

Result:
no goals
-- Mathlib/Algebra/DualNumber.lean
theorem lift_op_smul (fe : {fe : (A →ₐ[R] B) × B // _}) (a : A) (ad : A[ε]) :
    lift fe (MulOpposite.op a • ad) = lift fe ad * fe.val.1 a

Proof state:
R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }
a : A
ad : A[ε]
⊢ (lift fe) (MulOpposite.op a • ad) = (lift fe) ad * (↑fe).1 a

Tactic:
rw [← mul_inl_eq_op_smul, map_mul, lift_apply_inl]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem eq_of_add_eq_add_right {a b c : Cardinal} (h : a + b = c + b) (hb : b < ℵ₀) :
    a = c

Proof state:
a b c : Cardinal.{u_1}
h : b + a = b + c
hb : b < ℵ₀
⊢ a = c

Tactic:
exact Cardinal.eq_of_add_eq_add_left h hb

Result:
no goals

Proof state:
a b c : Cardinal.{u_1}
h : a + b = c + b
hb : b < ℵ₀
⊢ a = c

Tactic:
rw [add_comm a b, add_comm c b] at h

Result:
a b c : Cardinal.{u_1}
h : b + a = b + c
hb : b < ℵ₀
⊢ a = c
-- Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
@[reassoc]
lemma extendScalars_assoc :
    (extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom ≫ whiskerRight (extendScalarsComp f₁₂ f₂₃).hom _ =
      (extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom ≫ whiskerLeft _ (extendScalarsComp f₂₃ f₃₄).hom ≫
        (Functor.associator _ _ _).inv

Proof state:
case w.h.h
R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
M : ModuleCat R₁
m : ↑M
h₁ : (ConcreteCategory.hom ((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₃] 1 ⊗ₜ[R₁] m
h₂ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] 1 ⊗ₜ[R₁] m
h₃ :
  ∀ (M : ModuleCat R₂) (m : ↑M),
    (ConcreteCategory.hom ((extendScalarsComp f₂₃ f₃₄).hom.app M)) (1 ⊗ₜ[R₂] m) = 1 ⊗ₜ[R₃] 1 ⊗ₜ[R₂] m
h₄ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ f₂₃).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] 1 ⊗ₜ[R₁] m
⊢ (Hom.hom ((extendScalars f₃₄).map ((extendScalarsComp f₁₂ f₂₃).hom.app M))) (1 ⊗ₜ[R₃] 1 ⊗ₜ[R₁] m) =
    (Hom.hom ((extendScalarsComp f₂₃ f₃₄).hom.app ((extendScalars f₁₂).obj M)))
      ((Hom.hom ((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom.app M)) (1 ⊗ₜ[R₁] m))

Tactic:
erw [h₂]

Result:
case w.h.h
R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
M : ModuleCat R₁
m : ↑M
h₁ : (ConcreteCategory.hom ((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₃] 1 ⊗ₜ[R₁] m
h₂ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] 1 ⊗ₜ[R₁] m
h₃ :
  ∀ (M : ModuleCat R₂) (m : ↑M),
    (ConcreteCategory.hom ((extendScalarsComp f₂₃ f₃₄).hom.app M)) (1 ⊗ₜ[R₂] m) = 1 ⊗ₜ[R₃] 1 ⊗ₜ[R₂] m
h₄ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ f₂₃).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] 1 ⊗ₜ[R₁] m
⊢ (Hom.hom ((extendScalars f₃₄).map ((extendScalarsComp f₁₂ f₂₃).hom.app M))) (1 ⊗ₜ[R₃] 1 ⊗ₜ[R₁] m) =
    (Hom.hom ((extendScalarsComp f₂₃ f₃₄).hom.app ((extendScalars f₁₂).obj M))) (1 ⊗ₜ[R₂] 1 ⊗ₜ[R₁] m)
-- Mathlib/GroupTheory/Exponent.lean
theorem pow_eq_mod_exponent {n : ℕ} (g : G) : g ^ n = g ^ (n % exponent G) :=
  calc
    g ^ n = g ^ (n % exponent G + exponent G * (n / exponent G))

Proof state:
G : Type u
inst✝ : Monoid G
n : ℕ
g : G
⊢ g ^ (n % exponent G + exponent G * (n / exponent G)) = g ^ (n % exponent G)

Tactic:
simp [pow_add, pow_mul, pow_exponent_eq_one]

Result:
no goals

Proof state:
G : Type u
inst✝ : Monoid G
n : ℕ
g : G
⊢ g ^ n = g ^ (n % exponent G + exponent G * (n / exponent G))

Tactic:
rw [Nat.mod_add_div]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem normalize_mul_normalize (n₁ n₂) {d₁ d₂} (z₁ z₂) :
    normalize n₁ d₁ z₁ * normalize n₂ d₂ z₂ =
    normalize (n₁ * n₂) (d₁ * d₂) (Nat.mul_ne_zero z₁ z₂)

Proof state:
case mk'.intro.intro.intro.mk'.intro.intro.intro
num✝¹ : Int
den✝¹ : Nat
den_nz✝¹ : den✝¹ ≠ 0
reduced✝¹ : num✝¹.natAbs.Coprime den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) z₁ = { num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ }
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
g₂ : Nat
zg₂ : g₂ ≠ 0
z₂ : den✝ * g₂ ≠ 0
e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) z₂ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }
⊢ { num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ } *
      { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ } =
    normalize (num✝¹ * ↑g₁ * (num✝ * ↑g₂)) (den✝¹ * g₁ * (den✝ * g₂)) ⋯

Tactic:
simp only [mul_def]

Result:
case mk'.intro.intro.intro.mk'.intro.intro.intro
num✝¹ : Int
den✝¹ : Nat
den_nz✝¹ : den✝¹ ≠ 0
reduced✝¹ : num✝¹.natAbs.Coprime den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) z₁ = { num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ }
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
g₂ : Nat
zg₂ : g₂ ≠ 0
z₂ : den✝ * g₂ ≠ 0
e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) z₂ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }
⊢ normalize (num✝¹ * num✝) (den✝¹ * den✝) ⋯ = normalize (num✝¹ * ↑g₁ * (num✝ * ↑g₂)) (den✝¹ * g₁ * (den✝ * g₂)) ⋯

Proof state:
case mk'.intro.intro.intro.mk'.intro.intro.intro
num✝¹ : Int
den✝¹ : Nat
den_nz✝¹ : den✝¹ ≠ 0
reduced✝¹ : num✝¹.natAbs.Coprime den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) z₁ = { num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ }
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
g₂ : Nat
zg₂ : g₂ ≠ 0
z₂ : den✝ * g₂ ≠ 0
e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) z₂ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }
⊢ normalize (num✝¹ * num✝) (den✝¹ * den✝) ⋯ = normalize (num✝¹ * ↑g₁ * (num✝ * ↑g₂)) (den✝¹ * g₁ * (den✝ * g₂)) ⋯

Tactic:
rw [← normalize_mul_right _ (Nat.mul_ne_zero zg₁ zg₂)]

Result:
case mk'.intro.intro.intro.mk'.intro.intro.intro
num✝¹ : Int
den✝¹ : Nat
den_nz✝¹ : den✝¹ ≠ 0
reduced✝¹ : num✝¹.natAbs.Coprime den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) z₁ = { num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ }
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
g₂ : Nat
zg₂ : g₂ ≠ 0
z₂ : den✝ * g₂ ≠ 0
e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) z₂ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }
⊢ normalize (num✝¹ * num✝ * ↑(g₁ * g₂)) (den✝¹ * den✝ * (g₁ * g₂)) ⋯ =
    normalize (num✝¹ * ↑g₁ * (num✝ * ↑g₂)) (den✝¹ * g₁ * (den✝ * g₂)) ⋯
-- Mathlib/Data/Matroid/Circuit.lean
lemma isCircuit_iff : M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃D⦄, M.Dep D → D ⊆ C → D = C

Proof state:
α : Type u_1
M : Matroid α
C : Set α
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C

Tactic:
simp_rw [isCircuit_def, minimal_subset_iff, eq_comm (a := C)]

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr₂_eq_map₂_of_constant_state (f : α → β → σ → σ × γ) (s : σ)
    (h : ∀ a b, (f a b s).fst = s) :
    mapAccumr₂ f xs ys s = (s, (map₂ (fun x y => (f x y s).snd) xs ys))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s : σ
h : ∀ (a : α) (b : β), (f a b s).1 = s
⊢ mapAccumr₂ f xs ys s = (s, map₂ (fun x y => (f x y s).2) xs ys)

Tactic:
induction xs, ys using revInductionOn₂ <;> simp_all

Result:
no goals
-- Mathlib/RingTheory/Trace/Defs.lean
theorem trace_eq_zero_of_not_exists_basis (h : ¬∃ s : Finset S, Nonempty (Basis s R S)) :
    trace R S = 0

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : ¬∃ s, Nonempty (Basis { x // x ∈ s } R S)
s : S
⊢ (trace R S) s = 0 s

Tactic:
simp [trace_apply, LinearMap.trace, h]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : ¬∃ s, Nonempty (Basis { x // x ∈ s } R S)
⊢ trace R S = 0

Tactic:
ext s

Result:
case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : ¬∃ s, Nonempty (Basis { x // x ∈ s } R S)
s : S
⊢ (trace R S) s = 0 s
-- Mathlib/Data/Fin/Basic.lean
@[simp]
lemma succAbove_ne_zero_zero [NeZero n] {a : Fin (n + 1)} (ha : a ≠ 0) : a.succAbove 0 = 0

Proof state:
n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ castSucc 0 = 0

Tactic:
exact castSucc_zero'

Result:
no goals

Proof state:
case h
n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ castSucc 0 < a

Tactic:
exact Fin.pos_iff_ne_zero.2 ha

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ a.succAbove 0 = 0

Tactic:
rw [Fin.succAbove_of_castSucc_lt]

Result:
n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ castSucc 0 = 0

case h
n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ castSucc 0 < a
-- Mathlib/RingTheory/WittVector/WittPolynomial.lean
theorem wittPolynomial_vars_subset (n : ℕ) : (wittPolynomial p R n).vars ⊆ range (n + 1)

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : NeZero p
n : ℕ
⊢ ((map (Int.castRingHom R)) (W_ ℤ n)).vars ⊆ (W_ ℤ n).vars

Tactic:
apply vars_map

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : NeZero p
n : ℕ
⊢ (W_ R n).vars ⊆ range (n + 1)

Tactic:
rw [← map_wittPolynomial p (Int.castRingHom R), ← wittPolynomial_vars p ℤ]

Result:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : NeZero p
n : ℕ
⊢ ((map (Int.castRingHom R)) (W_ ℤ n)).vars ⊆ (W_ ℤ n).vars
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem contains_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
    (Const.alter m k f).contains k = (f (Const.get? m k)).isSome

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : Option β → Option β
⊢ (alter m k f).contains k = (f (get? m k)).isSome

Tactic:
simp only [contains_alter, BEq.refl, reduceIte]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
@[simp] lemma range_two_mul_add_one (α : Type*) [Semiring α] :
    Set.range (fun x : α ↦ 2 * x + 1) = {a | Odd a}

Proof state:
case h
α : Type u_4
inst✝ : Semiring α
x : α
⊢ (x ∈ Set.range fun x => 2 * x + 1) ↔ x ∈ {a | Odd a}

Tactic:
simp [Odd, eq_comm]

Result:
no goals

Proof state:
α : Type u_4
inst✝ : Semiring α
⊢ (Set.range fun x => 2 * x + 1) = {a | Odd a}

Tactic:
ext x

Result:
case h
α : Type u_4
inst✝ : Semiring α
x : α
⊢ (x ∈ Set.range fun x => 2 * x + 1) ↔ x ∈ {a | Odd a}