harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/TensorProduct/Basis.lean
/-- Elements in `M ⊗ N` can be represented by sum of elements of basis of `M` tensor elements of
  `N`. -/
lemma TensorProduct.eq_repr_basis_left :
    ∃ (c : ι →₀ N), (c.sum fun i n ↦ ℬ i ⊗ₜ n) = x

Proof state:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ℬ : Basis ι R M
c : ι →₀ N
⊢ (TensorProduct.comm R M N) (c.sum fun i n => ℬ i ⊗ₜ[R] n) =
    (TensorProduct.comm R M N) ((equivFinsuppOfBasisLeft ℬ).symm c)

Tactic:
simp [Finsupp.sum]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ℬ : Basis ι R M
x : M ⊗[R] N
⊢ ∃ c, (c.sum fun i n => ℬ i ⊗ₜ[R] n) = x

Tactic:
obtain ⟨c, rfl⟩ := (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm.surjective x

Result:
case intro
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ℬ : Basis ι R M
c : ι →₀ N
⊢ ∃ c_1, (c_1.sum fun i n => ℬ i ⊗ₜ[R] n) = (equivFinsuppOfBasisLeft ℬ).symm c

Proof state:
case intro
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ℬ : Basis ι R M
c : ι →₀ N
⊢ ∃ c_1, (c_1.sum fun i n => ℬ i ⊗ₜ[R] n) = (equivFinsuppOfBasisLeft ℬ).symm c

Tactic:
exact ⟨c, (TensorProduct.comm R M N).injective <| by simp [Finsupp.sum]⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ℬ : Basis ι R M
x : M ⊗[R] N
⊢ ∃ c, (c.sum fun i n => ℬ i ⊗ₜ[R] n) = x

Tactic:
classical obtain ⟨c, rfl⟩ := (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm.surjective x

Result:
case intro
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ℬ : Basis ι R M
c : ι →₀ N
⊢ ∃ c_1, (c_1.sum fun i n => ℬ i ⊗ₜ[R] n) = (equivFinsuppOfBasisLeft ℬ).symm c
-- Mathlib/SetTheory/Game/PGame.lean
theorem neg_insertRight_neg (x x' : PGame.{u}) : (-x).insertRight (-x') = -x.insertLeft x'

Proof state:
case mk
x' : PGame
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ (-mk α✝ β✝ a✝¹ a✝).insertRight (-x') = -(mk α✝ β✝ a✝¹ a✝).insertLeft x'

Tactic:
cases x'

Result:
case mk.mk
α✝¹ β✝¹ : Type u
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ (-mk α✝¹ β✝¹ a✝³ a✝²).insertRight (-mk α✝ β✝ a✝¹ a✝) = -(mk α✝¹ β✝¹ a✝³ a✝²).insertLeft (mk α✝ β✝ a✝¹ a✝)

Proof state:
case mk.mk
α✝¹ β✝¹ : Type u
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ mk β✝¹ (α✝¹ ⊕ PUnit.{u + 1}) (fun x => -a✝² x)
      (Sum.elim (fun x => -a✝³ x) fun x => mk β✝ α✝ (fun x => -a✝ x) fun x => -a✝¹ x) =
    mk β✝¹ (α✝¹ ⊕ PUnit.{u + 1}) (fun x => -a✝² x) fun x => -Sum.elim a✝³ (fun x => mk α✝ β✝ a✝¹ a✝) x

Tactic:
congr! with (i | j)

Result:
no goals

Proof state:
case mk.mk
α✝¹ β✝¹ : Type u
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ (-mk α✝¹ β✝¹ a✝³ a✝²).insertRight (-mk α✝ β✝ a✝¹ a✝) = -(mk α✝¹ β✝¹ a✝³ a✝²).insertLeft (mk α✝ β✝ a✝¹ a✝)

Tactic:
dsimp [insertRight, insertLeft]

Result:
case mk.mk
α✝¹ β✝¹ : Type u
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ mk β✝¹ (α✝¹ ⊕ PUnit.{u + 1}) (fun x => -a✝² x)
      (Sum.elim (fun x => -a✝³ x) fun x => mk β✝ α✝ (fun x => -a✝ x) fun x => -a✝¹ x) =
    mk β✝¹ (α✝¹ ⊕ PUnit.{u + 1}) (fun x => -a✝² x) fun x => -Sum.elim a✝³ (fun x => mk α✝ β✝ a✝¹ a✝) x

Proof state:
x x' : PGame
⊢ (-x).insertRight (-x') = -x.insertLeft x'

Tactic:
cases x

Result:
case mk
x' : PGame
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ (-mk α✝ β✝ a✝¹ a✝).insertRight (-x') = -(mk α✝ β✝ a✝¹ a✝).insertLeft x'
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
    (m.erase k).contains a = (!(k == a) && m.contains a)

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
⊢ (m.erase k).contains a = (!k == a && m.contains a)

Tactic:
simp_to_raw using Raw₀.contains_erase

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma Ψ_ofNat (n : ℕ) : W.Ψ n = C (W.preΨ' n) * if Even n then W.ψ₂ else 1

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ W.Ψ ↑n = C (W.preΨ' n) * if Even n then W.ψ₂ else 1

Tactic:
simp only [Ψ, preΨ_ofNat, Int.even_coe_nat]

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem Specializes.joinedIn (h : x ⤳ y) (hx : x ∈ F) (hy : y ∈ F) : JoinedIn F x y

Proof state:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
⊢ Continuous ({1}.piecewise (const (↑I) y) (const (↑I) x))

Tactic:
exact isClosed_singleton.continuous_piecewise_of_specializes continuous_const continuous_const
  fun _ ↦ h

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
⊢ { toFun := {1}.piecewise (const (↑I) y) (const (↑I) x), continuous_toFun := ?m.9555 }.toFun 1 = y

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
⊢ { toFun := {1}.piecewise (const (↑I) y) (const (↑I) x), continuous_toFun := ?m.9555 }.toFun 0 = x

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
⊢ JoinedIn F x y

Tactic:
refine ⟨⟨⟨Set.piecewise {1} (const I y) (const I x), ?_⟩, by simp, by simp⟩, fun t ↦ ?_⟩

Result:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
⊢ Continuous ({1}.piecewise (const (↑I) y) (const (↑I) x))

case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
t : ↑I
⊢ { toFun := {1}.piecewise (const (↑I) y) (const (↑I) x), continuous_toFun := ?refine_1, source' := ⋯, target' := ⋯ }
      t ∈
    F

Proof state:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
t : ↑I
⊢ { toFun := {1}.piecewise (const (↑I) y) (const (↑I) x), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } t ∈ F

Tactic:
simp only [Path.coe_mk_mk, piecewise]

Result:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
t : ↑I
⊢ (if t ∈ {1} then const (↑I) y t else const (↑I) x t) ∈ F

Proof state:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
t : ↑I
⊢ (if t ∈ {1} then const (↑I) y t else const (↑I) x t) ∈ F

Tactic:
split_ifs <;> assumption

Result:
no goals
-- Mathlib/Data/Real/Archimedean.lean
theorem iSup_const_zero : ⨆ _ : ι, (0 : ℝ) = 0

Proof state:
case inl
ι : Sort u_1
h✝ : IsEmpty ι
⊢ ⨆ x, 0 = 0

Tactic:
exact Real.iSup_of_isEmpty _

Result:
no goals

Proof state:
case inr
ι : Sort u_1
h✝ : Nonempty ι
⊢ ⨆ x, 0 = 0

Tactic:
exact ciSup_const

Result:
no goals

Proof state:
ι : Sort u_1
⊢ ⨆ x, 0 = 0

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
ι : Sort u_1
h✝ : IsEmpty ι
⊢ ⨆ x, 0 = 0

case inr
ι : Sort u_1
h✝ : Nonempty ι
⊢ ⨆ x, 0 = 0
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem inv_pow' (A : M) (n : ℕ) : A⁻¹ ^ n = (A ^ n)⁻¹

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ A⁻¹ ^ n = (A ^ n)⁻¹

Tactic:
induction n with
| zero => simp
| succ n ih => rw [pow_succ A, mul_inv_rev, ← ih, ← pow_succ']

Result:
no goals

Proof state:
case zero
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ A⁻¹ ^ 0 = (A ^ 0)⁻¹

Tactic:
simp

Result:
no goals

Proof state:
case succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
ih : A⁻¹ ^ n = (A ^ n)⁻¹
⊢ A⁻¹ ^ (n + 1) = (A ^ (n + 1))⁻¹

Tactic:
rw [pow_succ A, mul_inv_rev, ← ih, ← pow_succ']

Result:
no goals
-- Mathlib/LinearAlgebra/JordanChevalley.lean
theorem exists_isNilpotent_isSemisimple [PerfectField K] :
    ∃ᵉ (n ∈ adjoin K {f}) (s ∈ adjoin K {f}), IsNilpotent n ∧ IsSemisimple s ∧ f = n + s

Proof state:
K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
f : End K V
inst✝¹ : FiniteDimensional K V
inst✝ : PerfectField K
⊢ ∃ n ∈ adjoin K {f}, ∃ s ∈ adjoin K {f}, IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s

Tactic:
obtain ⟨g, k, sep, -, nil⟩ := exists_squarefree_dvd_pow_of_ne_zero (minpoly.ne_zero_of_finite K f)

Result:
case intro.intro.intro.intro
K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
f : End K V
inst✝¹ : FiniteDimensional K V
inst✝ : PerfectField K
g : K[X]
k : ℕ
sep : Squarefree g
nil : minpoly K f ∣ g ^ k
⊢ ∃ n ∈ adjoin K {f}, ∃ s ∈ adjoin K {f}, IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s

Proof state:
case intro.intro.intro.intro
K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
f : End K V
inst✝¹ : FiniteDimensional K V
inst✝ : PerfectField K
g : K[X]
k : ℕ
sep : Squarefree g
nil : minpoly K f ∣ g ^ k
⊢ ∃ n ∈ adjoin K {f}, ∃ s ∈ adjoin K {f}, IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s

Tactic:
rw [← PerfectField.separable_iff_squarefree] at sep

Result:
case intro.intro.intro.intro
K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
f : End K V
inst✝¹ : FiniteDimensional K V
inst✝ : PerfectField K
g : K[X]
k : ℕ
sep : g.Separable
nil : minpoly K f ∣ g ^ k
⊢ ∃ n ∈ adjoin K {f}, ∃ s ∈ adjoin K {f}, IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s

Proof state:
case intro.intro.intro.intro
K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
f : End K V
inst✝¹ : FiniteDimensional K V
inst✝ : PerfectField K
g : K[X]
k : ℕ
sep : g.Separable
nil : minpoly K f ∣ g ^ k
⊢ ∃ n ∈ adjoin K {f}, ∃ s ∈ adjoin K {f}, IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s

Tactic:
exact exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow sep nil

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem pmap_eq_some_iff {p : α → Prop} {f : ∀ (a : α), p a → β} {o : Option α} {h} :
    pmap f o h = some b ↔ ∃ (a : α) (h : p a), o = some a ∧ b = f a h

Proof state:
case some
α : Type u_1
β : Type u_2
b : β
p : α → Prop
f : (a : α) → p a → β
a : α
h : ∀ (a_1 : α), a_1 ∈ some a → p a_1
⊢ pmap f (some a) h = some b ↔ ∃ a_1 h, some a = some a_1 ∧ b = f a_1 h

Tactic:
simp only [pmap, eq_comm, some.injEq, exists_and_left, exists_eq_left']

Result:
case some
α : Type u_1
β : Type u_2
b : β
p : α → Prop
f : (a : α) → p a → β
a : α
h : ∀ (a_1 : α), a_1 ∈ some a → p a_1
⊢ b = f a ⋯ ↔ ∃ x, b = f a ⋯

Proof state:
case some
α : Type u_1
β : Type u_2
b : β
p : α → Prop
f : (a : α) → p a → β
a : α
h : ∀ (a_1 : α), a_1 ∈ some a → p a_1
⊢ b = f a ⋯ ↔ ∃ x, b = f a ⋯

Tactic:
constructor

Result:
case some.mp
α : Type u_1
β : Type u_2
b : β
p : α → Prop
f : (a : α) → p a → β
a : α
h : ∀ (a_1 : α), a_1 ∈ some a → p a_1
⊢ b = f a ⋯ → ∃ x, b = f a ⋯

case some.mpr
α : Type u_1
β : Type u_2
b : β
p : α → Prop
f : (a : α) → p a → β
a : α
h : ∀ (a_1 : α), a_1 ∈ some a → p a_1
⊢ (∃ x, b = f a ⋯) → b = f a ⋯

Proof state:
case some.mp
α : Type u_1
β : Type u_2
b : β
p : α → Prop
f : (a : α) → p a → β
a : α
h : ∀ (a_1 : α), a_1 ∈ some a → p a_1
⊢ b = f a ⋯ → ∃ x, b = f a ⋯

Tactic:
exact fun w => ⟨h a rfl, w⟩

Result:
no goals

Proof state:
case none
α : Type u_1
β : Type u_2
b : β
p : α → Prop
f : (a : α) → p a → β
h : ∀ (a : α), a ∈ none → p a
⊢ pmap f none h = some b ↔ ∃ a h, none = some a ∧ b = f a h

Tactic:
simp

Result:
no goals

Proof state:
case some.mpr
α : Type u_1
β : Type u_2
b : β
p : α → Prop
f : (a : α) → p a → β
a : α
h : ∀ (a_1 : α), a_1 ∈ some a → p a_1
⊢ (∃ x, b = f a ⋯) → b = f a ⋯

Tactic:
rintro ⟨h, rfl⟩

Result:
case some.mpr.intro
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
a : α
h✝ : ∀ (a_1 : α), a_1 ∈ some a → p a_1
h : p a
⊢ f a ⋯ = f a ⋯

Proof state:
case some.mpr.intro
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
a : α
h✝ : ∀ (a_1 : α), a_1 ∈ some a → p a_1
h : p a
⊢ f a ⋯ = f a ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/LocalAtTarget.lean
theorem isClosed_iff_coe_preimage {s : Set β} :
    IsClosed s ↔ ∀ i, IsClosed ((↑) ⁻¹' s : Set (U i))

Proof state:
β : Type u_2
inst✝ : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
s : Set β
⊢ IsClosed s ↔ ∀ (i : ι), IsClosed (Subtype.val ⁻¹' s)

Tactic:
simpa using hU.isOpen_iff_coe_preimage (s := sᶜ)

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiff_all_iff_nat : (∀ n : ℕ∞, ContDiff 𝕜 n f) ↔ ∀ n : ℕ, ContDiff 𝕜 n f

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
⊢ (∀ (n : ℕ∞), ContDiff 𝕜 (↑n) f) ↔ ∀ (n : ℕ), ContDiff 𝕜 (↑n) f

Tactic:
simp only [← contDiffOn_univ, contDiffOn_all_iff_nat]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mk_mem_zipIdx_iff_getElem? {x : α} {i : Nat} {l : Array α} :
    (x, i) ∈ l.zipIdx ↔ l[i]? = x

Proof state:
α : Type u_1
x : α
i : Nat
l : Array α
⊢ (x, i) ∈ l.zipIdx ↔ l[i]? = some x

Tactic:
rw [mk_mem_zipIdx_iff_le_and_getElem?_sub]

Result:
α : Type u_1
x : α
i : Nat
l : Array α
⊢ 0 ≤ i ∧ l[i - 0]? = some x ↔ l[i]? = some x

Proof state:
α : Type u_1
x : α
i : Nat
l : Array α
⊢ 0 ≤ i ∧ l[i - 0]? = some x ↔ l[i]? = some x

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean
lemma snd (h : LeftFraction₂Rel z₁ z₂) : LeftFractionRel z₁.snd z₂.snd

Proof state:
case intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.LeftFraction₂ X Y
Z : C
t₁ : z₁.Y' ⟶ Z
t₂ : z₂.Y' ⟶ Z
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
w✝ : z₁.f ≫ t₁ = z₂.f ≫ t₂
hft' : z₁.f' ≫ t₁ = z₂.f' ≫ t₂
ht : W (z₁.s ≫ t₁)
⊢ LeftFractionRel z₁.snd z₂.snd

Tactic:
exact ⟨Z, t₁, t₂, hst, hft', ht⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.LeftFraction₂ X Y
h : LeftFraction₂Rel z₁ z₂
⊢ LeftFractionRel z₁.snd z₂.snd

Tactic:
obtain ⟨Z, t₁, t₂, hst, _, hft', ht⟩ := h

Result:
case intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.LeftFraction₂ X Y
Z : C
t₁ : z₁.Y' ⟶ Z
t₂ : z₂.Y' ⟶ Z
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
w✝ : z₁.f ≫ t₁ = z₂.f ≫ t₂
hft' : z₁.f' ≫ t₁ = z₂.f' ≫ t₂
ht : W (z₁.s ≫ t₁)
⊢ LeftFractionRel z₁.snd z₂.snd
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma level_one' (hn : n = 1) : χ = 1

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
hn : n = 1
⊢ χ = 1

Tactic:
subst hn

Result:
R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R 1
⊢ χ = 1

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R 1
⊢ χ = 1

Tactic:
exact level_one _

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem iSup_eq_top_iff_toSubmodule {ι : Sort*} {N : ι → LieSubmodule R L M} :
    ⨆ i, N i = ⊤ ↔ ⨆ i, (N i : Submodule R M) = ⊤

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
N : ι → LieSubmodule R L M
⊢ ⨆ i, N i = ⊤ ↔ ⨆ i, ↑(N i) = ⊤

Tactic:
rw [← iSup_toSubmodule, ← top_toSubmodule (L := L), toSubmodule_inj]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem of_isLimit {c : PullbackCone f g} (h : Limits.IsLimit c) : IsPullback c.fst c.snd f g :=
  { w := c.condition
    isLimit' := ⟨IsLimit.ofIsoLimit h (Limits.PullbackCone.ext (Iso.refl _)
      (by simp) (by simp))⟩ }

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
h : IsLimit c
⊢ c.snd = (Iso.refl c.pt).hom ≫ (PullbackCone.mk c.fst c.snd ⋯).snd

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
h : IsLimit c
⊢ c.fst = (Iso.refl c.pt).hom ≫ (PullbackCone.mk c.fst c.snd ⋯).fst

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem boundary_zero : (c.boundary ⟨0, c.card_boundaries_pos⟩ : Fin (n + 1)) = 0

Proof state:
n : ℕ
c : CompositionAsSet n
⊢ c.boundary ⟨0, ⋯⟩ = 0

Tactic:
rw [boundary, Finset.orderEmbOfFin_zero rfl c.card_boundaries_pos]

Result:
n : ℕ
c : CompositionAsSet n
⊢ c.boundaries.min' ⋯ = 0

Proof state:
n : ℕ
c : CompositionAsSet n
⊢ c.boundaries.min' ⋯ = 0

Tactic:
exact le_antisymm (Finset.min'_le _ _ c.zero_mem) (Fin.zero_le _)

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem adjoin_adjoin_comm (T : Set E) :
    (adjoin (adjoin F S) T).restrictScalars F = (adjoin (adjoin F T) S).restrictScalars F

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ restrictScalars F (adjoin (↥(adjoin F S)) T) = restrictScalars F (adjoin (↥(adjoin F T)) S)

Tactic:
rw [adjoin_adjoin_left, adjoin_adjoin_left, Set.union_comm]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_add_right_eq_add (a b c : α) :
    toIcoMod hp a (b + c) = toIcoMod hp (a - c) b + c

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIcoMod hp a (b + c) = toIcoMod hp (a - c) b + c

Tactic:
simp_rw [toIcoMod, toIcoDiv_sub_eq_toIcoDiv_add', sub_add_eq_add_sub]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
lemma degree_C_mul_of_mul_ne_zero (h : a * p.leadingCoeff ≠ 0) : (C a * p).degree = p.degree

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ (C a).leadingCoeff * p.leadingCoeff ≠ 0

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ (C a * p).degree = p.degree

Tactic:
rw [degree_mul' (by simpa)]

Result:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ (C a).degree + p.degree = p.degree

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ (C a).degree + p.degree = p.degree

Tactic:
simp [left_ne_zero_of_mul h]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem Finite.infsep_of_nontrivial (hsf : s.Finite) (hs : s.Nontrivial) :
    s.infsep = hsf.offDiag.toFinset.inf' (by simpa) (uncurry dist)

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hsf : s.Finite
hs : s.Nontrivial
⊢ s.infsep = ⋯.toFinset.inf' ⋯ (uncurry dist)

Tactic:
simp_rw [hsf.infsep, dif_pos hs]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
hsf : s.Finite
hs : s.Nontrivial
⊢ ⋯.toFinset.Nonempty

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hsf : s.Finite
hs : s.Nontrivial
⊢ s.infsep = ⋯.toFinset.inf' ⋯ (uncurry dist)

Tactic:
classical simp_rw [hsf.infsep, dif_pos hs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_alter [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
    (m.alter k f).getKey? k' =
      if k == k' then
        if (f (m.get? k)).isSome then some k else none
      else
        m.getKey? k'

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ (m.alter k f).getKey? k' =
    if (k == k') = true then if (f (m.get? k)).isSome = true then some k else none else m.getKey? k'

Tactic:
simp_to_raw using Raw₀.getKey?_alter

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapFinIdx_eq_mapFinIdx_iff {l : List α} {f g : (i : Nat) → α → (h : i < l.length) → β} :
    l.mapFinIdx f = l.mapFinIdx g ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] h = g i l[i] h

Proof state:
α : Type u_1
β : Type u_2
l : List α
f g : (i : Nat) → α → i < l.length → β
⊢ (∃ h, ∀ (i : Nat) (h_1 : i < l.length), (l.mapFinIdx f)[i] = g i l[i] h_1) ↔
    ∀ (i : Nat) (h : i < l.length), f i l[i] h = g i l[i] h

Tactic:
simp [Fin.forall_iff]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : List α
f g : (i : Nat) → α → i < l.length → β
⊢ l.mapFinIdx f = l.mapFinIdx g ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] h = g i l[i] h

Tactic:
rw [eq_comm, mapFinIdx_eq_iff]

Result:
α : Type u_1
β : Type u_2
l : List α
f g : (i : Nat) → α → i < l.length → β
⊢ (∃ h, ∀ (i : Nat) (h_1 : i < l.length), (l.mapFinIdx f)[i] = g i l[i] h_1) ↔
    ∀ (i : Nat) (h : i < l.length), f i l[i] h = g i l[i] h
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem mul_nonsing_inv_cancel_left (B : Matrix n m α) (h : IsUnit A.det) : A * (A⁻¹ * B) = B

Proof state:
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
B : Matrix n m α
h : IsUnit A.det
⊢ A * (A⁻¹ * B) = B

Tactic:
simp [← Matrix.mul_assoc, mul_nonsing_inv A h]

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
lemma sup'_image₂_right (g : γ → δ) (h : (image₂ f s t).Nonempty) :
    sup' (image₂ f s t) h g =
      sup' t h.of_image₂_right fun y ↦ sup' s h.of_image₂_left (g <| f · y)

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : SemilatticeSup δ
g : γ → δ
h : (image₂ f s t).Nonempty
⊢ (image₂ f s t).sup' h g = t.sup' ⋯ fun y => s.sup' ⋯ fun x => g (f x y)

Tactic:
simp only [image₂, sup'_image, sup'_product_right]

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : SemilatticeSup δ
g : γ → δ
h : (image₂ f s t).Nonempty
⊢ (t.sup' ⋯ fun i' => s.sup' ⋯ fun i => (g ∘ uncurry f) (i, i')) = t.sup' ⋯ fun y => s.sup' ⋯ fun x => g (f x y)

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : SemilatticeSup δ
g : γ → δ
h : (image₂ f s t).Nonempty
⊢ (t.sup' ⋯ fun i' => s.sup' ⋯ fun i => (g ∘ uncurry f) (i, i')) = t.sup' ⋯ fun y => s.sup' ⋯ fun x => g (f x y)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Matrix/Basis.lean
theorem col_eq_zero_of_commute_stdBasisMatrix {i j k : n} {M : Matrix n n α}
    (hM : Commute (stdBasisMatrix i j 1) M) (hki : k ≠ i) : M k i = 0

Proof state:
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
i j k : n
M : Matrix n n α
hM : Commute (stdBasisMatrix i j 1) M
hki : k ≠ i
⊢ M k i = 0

Tactic:
have := ext_iff.mpr hM k j

Result:
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
i j k : n
M : Matrix n n α
hM : Commute (stdBasisMatrix i j 1) M
hki : k ≠ i
this : (stdBasisMatrix i j 1 * M) k j = (M * stdBasisMatrix i j 1) k j
⊢ M k i = 0

Proof state:
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
i j k : n
M : Matrix n n α
hM : Commute (stdBasisMatrix i j 1) M
hki : k ≠ i
this : (stdBasisMatrix i j 1 * M) k j = (M * stdBasisMatrix i j 1) k j
⊢ M k i = 0

Tactic:
aesop

Result:
no goals