harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem rename_hsymm (n : ℕ) (e : σ ≃ τ) : rename e (hsymm σ R n) = hsymm τ R n

Proof state:
case h
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
e : σ ≃ τ
⊢ ∀ (x : Sym σ n), (Multiset.map (fun x => X (e x)) ↑x).prod = (Multiset.map X ↑((equivCongr e) x)).prod

Tactic:
simp

Result:
no goals

Proof state:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
e : σ ≃ τ
⊢ (rename ⇑e) (hsymm σ R n) = hsymm τ R n

Tactic:
simp_rw [hsymm, map_sum, ← prod_hom', rename_X]

Result:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
e : σ ≃ τ
⊢ ∑ x : Sym σ n, (Multiset.map (fun x => X (e x)) ↑x).prod = ∑ s : Sym τ n, (Multiset.map X ↑s).prod

Proof state:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
e : σ ≃ τ
⊢ ∑ x : Sym σ n, (Multiset.map (fun x => X (e x)) ↑x).prod = ∑ s : Sym τ n, (Multiset.map X ↑s).prod

Tactic:
apply Fintype.sum_equiv (equivCongr e)

Result:
case h
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
e : σ ≃ τ
⊢ ∀ (x : Sym σ n), (Multiset.map (fun x => X (e x)) ↑x).prod = (Multiset.map X ↑((equivCongr e) x)).prod
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey_modify_self (h : m.1.WF) [Inhabited α] {k : α} {f : β k → β k}
    (hc : (m.modify k f).contains k) : (m.modify k f).getKey k hc = k

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
inst✝ : Inhabited α
k : α
f : β k → β k
hc : (m.modify k f).contains k = true
⊢ (m.modify k f).getKey k hc = k

Tactic:
simp_to_model [modify] using List.getKey_modifyKey_self

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem prod_mk_left (a : α) : LipschitzWith 1 (Prod.mk a : β → α × β)

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
a : α
⊢ LipschitzWith 1 (Prod.mk a)

Tactic:
simpa only [max_eq_right zero_le_one] using (LipschitzWith.const a).prod LipschitzWith.id

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem all_eq_false' {p : α → Bool} {xs : Vector α n} :
    xs.all p = false ↔ ∃ x, x ∈ xs ∧ ¬p x

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ { toArray := xs, size_toArray := ⋯ }.all p = false ↔ ∃ x, x ∈ { toArray := xs, size_toArray := ⋯ } ∧ ¬p x = true

Tactic:
simp only [all_mk, Array.all_eq_false']

Result:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ (∃ x, x ∈ xs ∧ ¬p x = true) ↔ ∃ x, x ∈ { toArray := xs, size_toArray := ⋯ } ∧ ¬p x = true

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ (∃ x, x ∈ xs ∧ ¬p x = true) ↔ ∃ x, x ∈ { toArray := xs, size_toArray := ⋯ } ∧ ¬p x = true

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
p : α → Bool
xs : Vector α n
⊢ xs.all p = false ↔ ∃ x, x ∈ xs ∧ ¬p x = true

Tactic:
rcases xs with ⟨xs, rfl⟩

Result:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ { toArray := xs, size_toArray := ⋯ }.all p = false ↔ ∃ x, x ∈ { toArray := xs, size_toArray := ⋯ } ∧ ¬p x = true
-- Mathlib/Data/Real/ConjExponents.lean
lemma isConjExponent_iff_eq_conjExponent (hp : 1 ≤ p) : p.IsConjExponent q ↔ q = 1 + (p - 1)⁻¹ :=
  ⟨fun h ↦ h.conj_eq, by rintro rfl; exact .conjExponent hp⟩

Proof state:
p q : ℝ≥0∞
hp : 1 ≤ p
⊢ q = 1 + (p - 1)⁻¹ → p.IsConjExponent q

Tactic:
rintro rfl

Result:
p : ℝ≥0∞
hp : 1 ≤ p
⊢ p.IsConjExponent (1 + (p - 1)⁻¹)

Proof state:
p : ℝ≥0∞
hp : 1 ≤ p
⊢ p.IsConjExponent (1 + (p - 1)⁻¹)

Tactic:
exact .conjExponent hp

Result:
no goals
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp.lean
theorem iso_isometry {V W : SemiNormedGrp₁} (i : V ≅ W) : Isometry i.hom

Proof state:
V W : SemiNormedGrp₁
i : V ≅ W
⊢ Isometry ⇑↑(Hom.hom i.hom)

Tactic:
change Isometry (⟨⟨i.hom, map_zero _⟩, fun _ _ => map_add _ _ _⟩ : V →+ W)

Result:
V W : SemiNormedGrp₁
i : V ≅ W
⊢ Isometry ⇑{ toFun := ⇑↑(Hom.hom i.hom), map_zero' := ⋯, map_add' := ⋯ }

Proof state:
V W : SemiNormedGrp₁
i : V ≅ W
v : V.carrier
⊢ ‖v‖ = ‖↑(Hom.hom i.inv) (↑(Hom.hom i.hom) v)‖

Tactic:
rw [← comp_apply, Iso.hom_inv_id, id_apply]

Result:
no goals

Proof state:
V W : SemiNormedGrp₁
i : V ≅ W
v : V.carrier
⊢ ‖{ toFun := ⇑↑(Hom.hom i.hom), map_zero' := ⋯, map_add' := ⋯ } v‖ = ‖v‖

Tactic:
apply le_antisymm (i.hom.2 v)

Result:
V W : SemiNormedGrp₁
i : V ≅ W
v : V.carrier
⊢ ‖v‖ ≤ ‖i.hom.hom' v‖

Proof state:
V W : SemiNormedGrp₁
i : V ≅ W
v : V.carrier
⊢ ‖v‖ ≤ ‖i.hom.hom' v‖

Tactic:
calc
  ‖v‖ = ‖i.inv (i.hom v)‖ := by rw [← comp_apply, Iso.hom_inv_id, id_apply]
  _ ≤ ‖i.hom v‖ := i.inv.2 _

Result:
no goals

Proof state:
V W : SemiNormedGrp₁
i : V ≅ W
⊢ Isometry ⇑{ toFun := ⇑↑(Hom.hom i.hom), map_zero' := ⋯, map_add' := ⋯ }

Tactic:
refine AddMonoidHomClass.isometry_of_norm _ ?_

Result:
V W : SemiNormedGrp₁
i : V ≅ W
⊢ ∀ (x : V.carrier), ‖{ toFun := ⇑↑(Hom.hom i.hom), map_zero' := ⋯, map_add' := ⋯ } x‖ = ‖x‖

Proof state:
V W : SemiNormedGrp₁
i : V ≅ W
⊢ ∀ (x : V.carrier), ‖{ toFun := ⇑↑(Hom.hom i.hom), map_zero' := ⋯, map_add' := ⋯ } x‖ = ‖x‖

Tactic:
intro v

Result:
V W : SemiNormedGrp₁
i : V ≅ W
v : V.carrier
⊢ ‖{ toFun := ⇑↑(Hom.hom i.hom), map_zero' := ⋯, map_add' := ⋯ } v‖ = ‖v‖
-- Mathlib/Algebra/Order/Sub/Basic.lean
theorem tsub_add_eq_max : a - b + b = max a b

Proof state:
case inr
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : b ≤ a
⊢ a - b + b = a ⊔ b

Tactic:
rw [max_eq_left h, tsub_add_cancel_of_le h]

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ a - b + b = a ⊔ b

Tactic:
rw [max_eq_right h, tsub_eq_zero_of_le h, zero_add]

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a - b + b = a ⊔ b

Tactic:
rcases le_total a b with h | h

Result:
case inl
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ a - b + b = a ⊔ b

case inr
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : b ≤ a
⊢ a - b + b = a ⊔ b
-- Mathlib/Topology/Sequences.lean
theorem SequentialSpace.iSup {X} {ι : Sort*} {t : ι → TopologicalSpace X}
    (h : ∀ i, @SequentialSpace X (t i)) : @SequentialSpace X (⨆ i, t i)

Proof state:
X : Type u_4
ι : Sort u_3
t : ι → TopologicalSpace X
h : ∀ (i : ι), SequentialSpace X
⊢ SequentialSpace X

Tactic:
letI : TopologicalSpace X := ⨆ i, t i

Result:
X : Type u_4
ι : Sort u_3
t : ι → TopologicalSpace X
h : ∀ (i : ι), SequentialSpace X
this : TopologicalSpace X := ⨆ i, t i
⊢ SequentialSpace X

Proof state:
X : Type u_4
ι : Sort u_3
t : ι → TopologicalSpace X
h : ∀ (i : ι), SequentialSpace X
this : TopologicalSpace X := ⨆ i, t i
⊢ SequentialSpace X

Tactic:
refine ⟨fun s hs ↦ isClosed_iSup_iff.2 fun i ↦ ?_⟩

Result:
X : Type u_4
ι : Sort u_3
t : ι → TopologicalSpace X
h : ∀ (i : ι), SequentialSpace X
this : TopologicalSpace X := ⨆ i, t i
s : Set X
hs : IsSeqClosed s
i : ι
⊢ IsClosed s

Proof state:
X : Type u_4
ι : Sort u_3
t : ι → TopologicalSpace X
h : ∀ (i : ι), SequentialSpace X
this✝ : TopologicalSpace X := ⨆ i, t i
s : Set X
hs : IsSeqClosed s
i : ι
this : TopologicalSpace X := t i
⊢ IsClosed s

Tactic:
exact IsSeqClosed.isClosed fun u x hus hux ↦ hs hus <| hux.mono_right <| nhds_mono <| le_iSup _ _

Result:
no goals

Proof state:
X : Type u_4
ι : Sort u_3
t : ι → TopologicalSpace X
h : ∀ (i : ι), SequentialSpace X
this : TopologicalSpace X := ⨆ i, t i
s : Set X
hs : IsSeqClosed s
i : ι
⊢ IsClosed s

Tactic:
letI := t i

Result:
X : Type u_4
ι : Sort u_3
t : ι → TopologicalSpace X
h : ∀ (i : ι), SequentialSpace X
this✝ : TopologicalSpace X := ⨆ i, t i
s : Set X
hs : IsSeqClosed s
i : ι
this : TopologicalSpace X := t i
⊢ IsClosed s
-- Mathlib/GroupTheory/Perm/Support.lean
theorem disjoint_refl_iff : Disjoint f f ↔ f = 1

Proof state:
case H
α : Type u_1
f : Perm α
h : f.Disjoint f
x : α
⊢ f x = 1 x

Tactic:
rcases h x with hx | hx <;> simp [hx]

Result:
no goals

Proof state:
α : Type u_1
f : Perm α
⊢ f.Disjoint f ↔ f = 1

Tactic:
refine ⟨fun h => ?_, fun h => h.symm ▸ disjoint_one_left 1⟩

Result:
α : Type u_1
f : Perm α
h : f.Disjoint f
⊢ f = 1

Proof state:
α : Type u_1
f : Perm α
h : f.Disjoint f
⊢ f = 1

Tactic:
ext x

Result:
case H
α : Type u_1
f : Perm α
h : f.Disjoint f
x : α
⊢ f x = 1 x
-- Mathlib/Data/Matrix/Basis.lean
theorem mem_range_scalar_iff_commute_stdBasisMatrix {M : Matrix n n α} :
    M ∈ Set.range (Matrix.scalar n) ↔ ∀ (i j : n), i ≠ j → Commute (stdBasisMatrix i j 1) M

Proof state:
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
⊢ M ∈ Set.range ⇑(scalar n) ↔ ∀ (i j : n), i ≠ j → Commute (stdBasisMatrix i j 1) M

Tactic:
refine ⟨fun ⟨r, hr⟩ i j _ => hr ▸ Commute.symm ?_, mem_range_scalar_of_commute_stdBasisMatrix⟩

Result:
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
x✝¹ : M ∈ Set.range ⇑(scalar n)
i j : n
x✝ : i ≠ j
r : α
hr : (scalar n) r = M
⊢ Commute ((scalar n) r) (stdBasisMatrix i j 1)

Proof state:
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
x✝¹ : M ∈ Set.range ⇑(scalar n)
i j : n
x✝ : i ≠ j
r : α
hr : (scalar n) r = M
⊢ Commute ((scalar n) r) (stdBasisMatrix i j 1)

Tactic:
rw [scalar_commute_iff]

Result:
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
x✝¹ : M ∈ Set.range ⇑(scalar n)
i j : n
x✝ : i ≠ j
r : α
hr : (scalar n) r = M
⊢ r • stdBasisMatrix i j 1 = MulOpposite.op r • stdBasisMatrix i j 1

Proof state:
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
x✝¹ : M ∈ Set.range ⇑(scalar n)
i j : n
x✝ : i ≠ j
r : α
hr : (scalar n) r = M
⊢ r • stdBasisMatrix i j 1 = MulOpposite.op r • stdBasisMatrix i j 1

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
/-- Every generalized eigenvector is a generalized eigenvector for exponent `finrank K V`.
(Lemma 8.11 of [axler2015]) -/
lemma genEigenspace_le_genEigenspace_finrank [FiniteDimensional K V] (f : End K V)
    (μ : K) (k : ℕ∞) : f.genEigenspace μ k ≤ f.genEigenspace μ (finrank K V)

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
k : ℕ∞
⊢ (f.genEigenspace μ) k ≤ (f.genEigenspace μ) ↑(finrank K V)

Tactic:
calc f.genEigenspace μ k
    ≤ f.genEigenspace μ ⊤ := (f.genEigenspace _).monotone le_top
  _ ≤ f.genEigenspace μ (finrank K V) := by
    rw [genEigenspace_top_eq_maxUnifEigenspaceIndex]
    exact (f.genEigenspace _).monotone <| by simpa using maxUnifEigenspaceIndex_le_finrank f μ

Result:
no goals

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
k : ℕ∞
⊢ (f.genEigenspace μ) ⊤ ≤ (f.genEigenspace μ) ↑(finrank K V)

Tactic:
rw [genEigenspace_top_eq_maxUnifEigenspaceIndex]

Result:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
k : ℕ∞
⊢ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ) ≤ (f.genEigenspace μ) ↑(finrank K V)

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
k : ℕ∞
⊢ ↑(f.maxUnifEigenspaceIndex μ) ≤ ↑(finrank K V)

Tactic:
simpa using maxUnifEigenspaceIndex_le_finrank f μ

Result:
no goals

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
k : ℕ∞
⊢ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ) ≤ (f.genEigenspace μ) ↑(finrank K V)

Tactic:
exact (f.genEigenspace _).monotone <| by simpa using maxUnifEigenspaceIndex_le_finrank f μ

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem derivWithin_add_const (c : F) :
    derivWithin (fun y => f y + c) s x = derivWithin f s x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
c : F
⊢ derivWithin (fun y => f y + c) s x = derivWithin f s x

Tactic:
simp only [derivWithin, fderivWithin_add_const]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem val_coe_unit_coprime {n : ℕ} (u : (ZMod n)ˣ) : Nat.Coprime (u : ZMod n).val n

Proof state:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ ↑((↑u).val * (↑u⁻¹).val) = ↑(u * u⁻¹)

Tactic:
rw [← natCast_zmod_val ((u * u⁻¹ : Units (ZMod (n + 1))) : ZMod (n + 1))]

Result:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ ↑((↑u).val * (↑u⁻¹).val) = ↑(↑(u * u⁻¹)).val

Proof state:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ (↑u).val.Coprime (n + 1)

Tactic:
apply Nat.coprime_of_mul_modEq_one ((u⁻¹ : Units (ZMod (n + 1))) : ZMod (n + 1)).val

Result:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ (↑u).val * (↑u⁻¹).val ≡ 1 [MOD n + 1]

Proof state:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ ↑((↑u).val * (↑u⁻¹).val) = ↑(↑(u * u⁻¹)).val

Tactic:
rw [Units.val_mul, val_mul, natCast_mod]

Result:
no goals

Proof state:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
this : ↑(u * u⁻¹) = 1
⊢ (↑u).val * (↑u⁻¹).val ≡ 1 [MOD n + 1]

Tactic:
rw [← eq_iff_modEq_nat, Nat.cast_one, ← this]

Result:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
this : ↑(u * u⁻¹) = 1
⊢ ↑((↑u).val * (↑u⁻¹).val) = ↑(u * u⁻¹)

Proof state:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
this : ↑(u * u⁻¹) = ↑1
⊢ (↑u).val * (↑u⁻¹).val ≡ 1 [MOD n + 1]

Tactic:
rw [Units.val_one] at this

Result:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
this : ↑(u * u⁻¹) = 1
⊢ (↑u).val * (↑u⁻¹).val ≡ 1 [MOD n + 1]

Proof state:
n : ℕ
u : (ZMod n)ˣ
⊢ (↑u).val.Coprime n

Tactic:
rcases n with - | n

Result:
case zero
u : (ZMod 0)ˣ
⊢ (↑u).val.Coprime 0

case succ
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ (↑u).val.Coprime (n + 1)

Proof state:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ (↑u).val * (↑u⁻¹).val ≡ 1 [MOD n + 1]

Tactic:
have := Units.ext_iff.1 (mul_inv_cancel u)

Result:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
this : ↑(u * u⁻¹) = ↑1
⊢ (↑u).val * (↑u⁻¹).val ≡ 1 [MOD n + 1]

Proof state:
case zero
u : (ZMod 0)ˣ
⊢ (↑u).val.Coprime 0

Tactic:
rcases Int.units_eq_one_or u with (rfl | rfl) <;> simp

Result:
no goals

Proof state:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
this : ↑(u * u⁻¹) = 1
⊢ ↑((↑u).val * (↑u⁻¹).val) = ↑(u * u⁻¹)

Tactic:
clear this

Result:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ ↑((↑u).val * (↑u⁻¹).val) = ↑(u * u⁻¹)
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem sum_repr_mul_repr {ι'} [Fintype ι'] (b' : Basis ι' R M) (x : M) (i : ι) :
    (∑ j : ι', b.repr (b' j) i * b'.repr x j) = b.repr x i

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
ι' : Type u_10
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
⊢ ∑ j : ι', (b.repr (b' j)) i * (b'.repr x) j = ∑ k : ι', ((b'.repr x) k • b.repr (b' k)) i

Tactic:
refine Finset.sum_congr rfl fun j _ => ?_

Result:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
ι' : Type u_10
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
j : ι'
x✝ : j ∈ Finset.univ
⊢ (b.repr (b' j)) i * (b'.repr x) j = ((b'.repr x) j • b.repr (b' j)) i

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
ι' : Type u_10
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
⊢ ∑ j : ι', (b.repr (b' j)) i * (b'.repr x) j = (b.repr (∑ i : ι', (b'.repr x) i • b' i)) i

Tactic:
simp_rw [map_sum, map_smul, Finset.sum_apply']

Result:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
ι' : Type u_10
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
⊢ ∑ j : ι', (b.repr (b' j)) i * (b'.repr x) j = ∑ k : ι', ((b'.repr x) k • b.repr (b' k)) i

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
ι' : Type u_10
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
j : ι'
x✝ : j ∈ Finset.univ
⊢ (b.repr (b' j)) i * (b'.repr x) j = ((b'.repr x) j • b.repr (b' j)) i

Tactic:
rw [Finsupp.smul_apply, smul_eq_mul, mul_comm]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
ι' : Type u_10
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
⊢ ∑ j : ι', (b.repr (b' j)) i * (b'.repr x) j = (b.repr x) i

Tactic:
conv_rhs => rw [← b'.sum_repr x]

Result:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
ι' : Type u_10
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
⊢ ∑ j : ι', (b.repr (b' j)) i * (b'.repr x) j = (b.repr (∑ i : ι', (b'.repr x) i • b' i)) i
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma map_eq_of_map_eq {W} {X Y : C}
    (φ₁ φ₂ : W.LeftFraction X Y) {E : Type*} [Category E]
    (L₁ : C ⥤ D) (L₂ : C ⥤ E) [L₁.IsLocalization W] [L₂.IsLocalization W]
    (h : φ₁.map L₁ (Localization.inverts L₁ W) = φ₂.map L₁ (Localization.inverts L₁ W)) :
    φ₁.map L₂ (Localization.inverts L₂ W) = φ₂.map L₂ (Localization.inverts L₂ W)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_6, u_2} D
W : MorphismProperty C
X Y : C
φ₁ φ₂ : W.LeftFraction X Y
E : Type u_3
inst✝² : Category.{u_5, u_3} E
L₁ : C ⥤ D
L₂ : C ⥤ E
inst✝¹ : L₁.IsLocalization W
inst✝ : L₂.IsLocalization W
h : φ₁.map L₁ ⋯ = φ₂.map L₁ ⋯
⊢ φ₁.map L₂ ⋯ = φ₂.map L₂ ⋯

Tactic:
apply (Localization.uniq L₂ L₁ W).functor.map_injective

Result:
case a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_6, u_2} D
W : MorphismProperty C
X Y : C
φ₁ φ₂ : W.LeftFraction X Y
E : Type u_3
inst✝² : Category.{u_5, u_3} E
L₁ : C ⥤ D
L₂ : C ⥤ E
inst✝¹ : L₁.IsLocalization W
inst✝ : L₂.IsLocalization W
h : φ₁.map L₁ ⋯ = φ₂.map L₁ ⋯
⊢ (Localization.uniq L₂ L₁ W).functor.map (φ₁.map L₂ ⋯) = (Localization.uniq L₂ L₁ W).functor.map (φ₂.map L₂ ⋯)

Proof state:
case a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_6, u_2} D
W : MorphismProperty C
X Y : C
φ₁ φ₂ : W.LeftFraction X Y
E : Type u_3
inst✝² : Category.{u_5, u_3} E
L₁ : C ⥤ D
L₂ : C ⥤ E
inst✝¹ : L₁.IsLocalization W
inst✝ : L₂.IsLocalization W
h : φ₁.map L₁ ⋯ = φ₂.map L₁ ⋯
⊢ (Localization.uniq L₂ L₁ W).functor.map (φ₁.map L₂ ⋯) = (Localization.uniq L₂ L₁ W).functor.map (φ₂.map L₂ ⋯)

Tactic:
rw [map_compatibility φ₁ L₂ L₁, map_compatibility φ₂ L₂ L₁, h]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Linear.lean
@[simp]
lemma cyclesMap'_smul :
    cyclesMap' (a • φ) h₁ h₂ = a • cyclesMap' φ h₁ h₂

Proof state:
R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
a : R
γ : LeftHomologyMapData φ h₁ h₂
⊢ cyclesMap' (a • φ) h₁ h₂ = a • cyclesMap' φ h₁ h₂

Tactic:
simp only [(γ.smul a).cyclesMap'_eq, LeftHomologyMapData.smul_φK, γ.cyclesMap'_eq]

Result:
no goals

Proof state:
R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
a : R
⊢ cyclesMap' (a • φ) h₁ h₂ = a • cyclesMap' φ h₁ h₂

Tactic:
have γ : LeftHomologyMapData φ h₁ h₂ := default

Result:
R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
a : R
γ : LeftHomologyMapData φ h₁ h₂
⊢ cyclesMap' (a • φ) h₁ h₂ = a • cyclesMap' φ h₁ h₂
-- Mathlib/Data/List/TakeWhile.lean
lemma find?_not_eq_head?_dropWhile :
    l.find? (fun x ↦ ! (p x)) = (l.dropWhile p).head?

Proof state:
case h.e'_3.h.e'_2.h.e'_2.h
α : Type u_1
p : α → Bool
l : List α
x✝ : α
⊢ p x✝ = !!p x✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ find? (fun x => !p x) l = (dropWhile p l).head?

Tactic:
convert l.find?_eq_head?_dropWhile_not ?_

Result:
case h.e'_3.h.e'_2.h.e'_2.h
α : Type u_1
p : α → Bool
l : List α
x✝ : α
⊢ p x✝ = !!p x✝
-- Mathlib/SetTheory/Ordinal/Enum.lean
theorem enumOrd_univ : enumOrd Set.univ = id

Proof state:
⊢ enumOrd (range id) = id

Tactic:
exact enumOrd_range strictMono_id

Result:
no goals

Proof state:
⊢ enumOrd Set.univ = id

Tactic:
rw [← range_id]

Result:
⊢ enumOrd (range id) = id
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_foldr_sup (l : List (L.BoundedFormula α n)) (v : α → M) (xs : Fin n → M) :
    (l.foldr (· ⊔ ·) ⊥).Realize v xs ↔ ∃ φ ∈ l, BoundedFormula.Realize φ v xs

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
l : List (L.BoundedFormula α n)
v : α → M
xs : Fin n → M
⊢ (List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ l).Realize v xs ↔ ∃ φ ∈ l, φ.Realize v xs

Tactic:
induction' l with φ l ih

Result:
case nil
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
⊢ (List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ []).Realize v xs ↔ ∃ φ ∈ [], φ.Realize v xs

case cons
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
φ : L.BoundedFormula α n
l : List (L.BoundedFormula α n)
ih : (List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ l).Realize v xs ↔ ∃ φ ∈ l, φ.Realize v xs
⊢ (List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (φ :: l)).Realize v xs ↔ ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs

Proof state:
case nil
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
⊢ (List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ []).Realize v xs ↔ ∃ φ ∈ [], φ.Realize v xs

Tactic:
simp

Result:
no goals

Proof state:
case cons
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
φ : L.BoundedFormula α n
l : List (L.BoundedFormula α n)
ih : (List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ l).Realize v xs ↔ ∃ φ ∈ l, φ.Realize v xs
⊢ (List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (φ :: l)).Realize v xs ↔ ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs

Tactic:
simp_rw [List.foldr_cons, realize_sup, ih, List.mem_cons, or_and_right, exists_or,
  exists_eq_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem attachWith_congr {l₁ l₂ : Vector α n} (w : l₁ = l₂) {P : α → Prop} {H : ∀ x ∈ l₁, P x} :
    l₁.attachWith P H = l₂.attachWith P fun _ h => H _ (w ▸ h)

Proof state:
α : Type u_1
n : Nat
l₁ l₂ : Vector α n
w : l₁ = l₂
P : α → Prop
H : ∀ (x : α), x ∈ l₁ → P x
⊢ l₁.attachWith P H = l₂.attachWith P ⋯

Tactic:
subst w

Result:
α : Type u_1
n : Nat
l₁ : Vector α n
P : α → Prop
H : ∀ (x : α), x ∈ l₁ → P x
⊢ l₁.attachWith P H = l₁.attachWith P ⋯

Proof state:
α : Type u_1
n : Nat
l₁ : Vector α n
P : α → Prop
H : ∀ (x : α), x ∈ l₁ → P x
⊢ l₁.attachWith P H = l₁.attachWith P ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[reassoc (attr := simp)]
lemma inl_v_desc_f (p q : ℤ) (h : p + (-1) = q) :
    (inl φ).v p q h ≫ (desc φ α β eq).f q = α.v p q h

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
α : Cochain F K (-1)
β : G ⟶ K
eq : δ (-1) 0 α = Cochain.ofHom (φ ≫ β)
p q : ℤ
h : p + -1 = q
⊢ (inl φ).v p q h ≫ (desc φ α β eq).f q = α.v p q h

Tactic:
simp [desc]

Result:
no goals