harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Shift/SingleFunctors.lean
lemma shiftIso_add' (n m mn : A) (hnm : m + n = mn) (a a' a'' : A)
    (ha' : n + a = a') (ha'' : m + a' = a'') :
    F.shiftIso mn a a'' (by rw [← hnm, ← ha'', ← ha', add_assoc]) =
      isoWhiskerLeft _ (shiftFunctorAdd' D m n mn hnm) ≪≫ (Functor.associator _ _ _).symm ≪≫
        isoWhiskerRight (F.shiftIso m a' a'' ha'') _ ≪≫ F.shiftIso n a a' ha'

Proof state:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst✝⁷ : Category.{?u.13943, u_1} C
inst✝⁶ : Category.{?u.13947, u_2} D
inst✝⁵ : Category.{?u.13951, u_3} E
inst✝⁴ : Category.{?u.13955, u_4} E'
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift D A
inst✝¹ : HasShift E A
inst✝ : HasShift E' A
F G H : SingleFunctors C D A
n m mn : A
hnm : m + n = mn
a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
⊢ mn + a = a''

Tactic:
rw [← hnm, ← ha'', ← ha', add_assoc]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_7, u_1} C
inst✝² : Category.{u_6, u_2} D
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : SingleFunctors C D A
n m mn : A
hnm : m + n = mn
a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
⊢ F.shiftIso mn a a'' ⋯ =
    isoWhiskerLeft (F.functor a'') (shiftFunctorAdd' D m n mn hnm) ≪≫
      ((F.functor a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
        isoWhiskerRight (F.shiftIso m a' a'' ha'') (shiftFunctor D n) ≪≫ F.shiftIso n a a' ha'

Tactic:
subst hnm

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_7, u_1} C
inst✝² : Category.{u_6, u_2} D
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : SingleFunctors C D A
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
⊢ F.shiftIso (m + n) a a'' ⋯ =
    isoWhiskerLeft (F.functor a'') (shiftFunctorAdd' D m n (m + n) ⋯) ≪≫
      ((F.functor a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
        isoWhiskerRight (F.shiftIso m a' a'' ha'') (shiftFunctor D n) ≪≫ F.shiftIso n a a' ha'

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_7, u_1} C
inst✝² : Category.{u_6, u_2} D
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : SingleFunctors C D A
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
⊢ F.shiftIso (m + n) a a'' ⋯ =
    isoWhiskerLeft (F.functor a'') (shiftFunctorAdd' D m n (m + n) ⋯) ≪≫
      ((F.functor a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
        isoWhiskerRight (F.shiftIso m a' a'' ha'') (shiftFunctor D n) ≪≫ F.shiftIso n a a' ha'

Tactic:
rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftIso_add]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem adjugate_adjugate (A : Matrix n n α) (h : Fintype.card n ≠ 1) :
    adjugate (adjugate A) = det A ^ (Fintype.card n - 2) • A

Proof state:
case succ.succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det
⊢ A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'

Tactic:
apply is_reg.matrix

Result:
case succ.succ.a
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det
⊢ (fun x => A'.det • x) A'.adjugate.adjugate = (fun x => A'.det • x) (A'.det ^ (Fintype.card n - 2) • A')

Proof state:
case succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n' : ℕ
h_card : Fintype.card n = n' + 1
⊢ A.adjugate.adjugate = A.det ^ (n' + 1 - 2) • A

Tactic:
cases n'

Result:
case succ.zero
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
h_card : Fintype.card n = 0 + 1
⊢ A.adjugate.adjugate = A.det ^ (0 + 1 - 2) • A

case succ.succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
⊢ A.adjugate.adjugate = A.det ^ (n✝ + 1 + 1 - 2) • A
-- Mathlib/Topology/Constructions.lean
theorem ContinuousAt.comp₂_of_eq {f : Y × Z → W} {g : X → Y} {h : X → Z} {x : X} {y : Y × Z}
    (hf : ContinuousAt f y) (hg : ContinuousAt g x) (hh : ContinuousAt h x) (e : (g x, h x) = y) :
    ContinuousAt (fun x ↦ f (g x, h x)) x

Proof state:
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : Y × Z → W
g : X → Y
h : X → Z
x : X
y : Y × Z
hf : ContinuousAt f y
hg : ContinuousAt g x
hh : ContinuousAt h x
e : (g x, h x) = y
⊢ ContinuousAt (fun x => f (g x, h x)) x

Tactic:
rw [← e] at hf

Result:
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : Y × Z → W
g : X → Y
h : X → Z
x : X
y : Y × Z
hf : ContinuousAt f (g x, h x)
hg : ContinuousAt g x
hh : ContinuousAt h x
e : (g x, h x) = y
⊢ ContinuousAt (fun x => f (g x, h x)) x

Proof state:
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : Y × Z → W
g : X → Y
h : X → Z
x : X
y : Y × Z
hf : ContinuousAt f (g x, h x)
hg : ContinuousAt g x
hh : ContinuousAt h x
e : (g x, h x) = y
⊢ ContinuousAt (fun x => f (g x, h x)) x

Tactic:
exact hf.comp₂ hg hh

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
theorem sin_eq_one_iff {x : ℂ} : sin x = 1 ↔ ∃ k : ℤ, π / 2 + k * (2 * π) = x

Proof state:
x : ℂ
⊢ (∃ k, ↑k * (2 * ↑π) = x - ↑π / 2) ↔ ∃ k, ↑π / 2 + ↑k * (2 * ↑π) = x

Tactic:
simp only [eq_sub_iff_add_eq']

Result:
no goals

Proof state:
x : ℂ
⊢ sin x = 1 ↔ ∃ k, ↑π / 2 + ↑k * (2 * ↑π) = x

Tactic:
rw [← cos_sub_pi_div_two, cos_eq_one_iff]

Result:
x : ℂ
⊢ (∃ k, ↑k * (2 * ↑π) = x - ↑π / 2) ↔ ∃ k, ↑π / 2 + ↑k * (2 * ↑π) = x
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
/-- A nilpotent endomorphism has nilpotent eigenvalues.

See also `LinearMap.isNilpotent_trace_of_isNilpotent`. -/
lemma HasUnifEigenvalue.isNilpotent_of_isNilpotent [NoZeroSMulDivisors R M] {f : End R M}
    (hfn : IsNilpotent f) {μ : R} (hf : f.HasUnifEigenvalue μ 1) :
    IsNilpotent μ

Proof state:
case intro.intro
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
μ : R
hf : f.HasUnifEigenvalue μ 1
m : M
hm : f.HasUnifEigenvector μ 1 m
n : ℕ
hn : f ^ n = 0
⊢ IsNilpotent μ

Tactic:
exact ⟨n, by simpa [hn, hm.2, eq_comm (a := (0 : M))] using hm.pow_apply n⟩

Result:
no goals

Proof state:
case intro
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
hfn : IsNilpotent f
μ : R
hf : f.HasUnifEigenvalue μ 1
m : M
hm : f.HasUnifEigenvector μ 1 m
⊢ IsNilpotent μ

Tactic:
obtain ⟨n : ℕ, hn : f ^ n = 0⟩ := hfn

Result:
case intro.intro
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
μ : R
hf : f.HasUnifEigenvalue μ 1
m : M
hm : f.HasUnifEigenvector μ 1 m
n : ℕ
hn : f ^ n = 0
⊢ IsNilpotent μ

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
hfn : IsNilpotent f
μ : R
hf : f.HasUnifEigenvalue μ 1
⊢ IsNilpotent μ

Tactic:
obtain ⟨m : M, hm⟩ := hf.exists_hasUnifEigenvector

Result:
case intro
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
hfn : IsNilpotent f
μ : R
hf : f.HasUnifEigenvalue μ 1
m : M
hm : f.HasUnifEigenvector μ 1 m
⊢ IsNilpotent μ

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
μ : R
hf : f.HasUnifEigenvalue μ 1
m : M
hm : f.HasUnifEigenvector μ 1 m
n : ℕ
hn : f ^ n = 0
⊢ μ ^ n = 0

Tactic:
simpa [hn, hm.2, eq_comm (a := (0 : M))] using hm.pow_apply n

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mul_eq_max_of_aleph0_le_left {a b : Cardinal} (h : ℵ₀ ≤ a) (h' : b ≠ 0) :
    a * b = max a b

Proof state:
case h.e'_3
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
this : b ≤ a
⊢ a = a * 1

Tactic:
rw [mul_one]

Result:
no goals

Proof state:
case inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
this : b ≤ a
⊢ a ⊔ b ≤ a * b

Tactic:
rw [max_eq_left this]

Result:
case inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
this : b ≤ a
⊢ a ≤ a * b

Proof state:
case inl
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : ℵ₀ ≤ b
⊢ a * b = a ⊔ b

Tactic:
exact mul_eq_max h hb

Result:
no goals

Proof state:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
⊢ a * b = a ⊔ b

Tactic:
rcases le_or_lt ℵ₀ b with hb | hb

Result:
case inl
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : ℵ₀ ≤ b
⊢ a * b = a ⊔ b

case inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
⊢ a * b = a ⊔ b

Proof state:
case inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
⊢ a * b = a ⊔ b

Tactic:
refine (mul_le_max_of_aleph0_le_left h).antisymm ?_

Result:
case inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
⊢ a ⊔ b ≤ a * b

Proof state:
case inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
⊢ a ⊔ b ≤ a * b

Tactic:
have : b ≤ a := hb.le.trans h

Result:
case inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
this : b ≤ a
⊢ a ⊔ b ≤ a * b

Proof state:
case inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
this : b ≤ a
⊢ a ≤ a * b

Tactic:
convert mul_le_mul_left' (one_le_iff_ne_zero.mpr h') a

Result:
case h.e'_3
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
this : b ≤ a
⊢ a = a * 1
-- Mathlib/SetTheory/Game/State.lean
theorem turnBound_ne_zero_of_right_move {s t : S} (m : t ∈ r s) : turnBound s ≠ 0

Proof state:
S : Type u
inst✝ : State S
s t : S
m : t ∈ r s
⊢ turnBound s ≠ 0

Tactic:
intro h

Result:
S : Type u
inst✝ : State S
s t : S
m : t ∈ r s
h : turnBound s = 0
⊢ False

Proof state:
S : Type u
inst✝ : State S
s t✝ : S
m : t✝ ∈ r s
h : turnBound s = 0
t : turnBound t✝ < turnBound s
⊢ False

Tactic:
rw [h] at t

Result:
S : Type u
inst✝ : State S
s t✝ : S
m : t✝ ∈ r s
h : turnBound s = 0
t : turnBound t✝ < 0
⊢ False

Proof state:
S : Type u
inst✝ : State S
s t : S
m : t ∈ r s
h : turnBound s = 0
⊢ False

Tactic:
have t := right_bound m

Result:
S : Type u
inst✝ : State S
s t✝ : S
m : t✝ ∈ r s
h : turnBound s = 0
t : turnBound t✝ < turnBound s
⊢ False

Proof state:
S : Type u
inst✝ : State S
s t✝ : S
m : t✝ ∈ r s
h : turnBound s = 0
t : turnBound t✝ < 0
⊢ False

Tactic:
exact Nat.not_succ_le_zero _ t

Result:
no goals
-- Mathlib/Data/Finset/Update.lean
lemma restrict_updateFinset_of_subset {s t : Finset ι} (hst : s ⊆ t) (x : Π i, π i)
    (y : Π i : t, π i) : s.restrict (updateFinset x t y) = restrict₂ hst y

Proof state:
case h
ι : Type u_1
π : ι → Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
hst : s ⊆ t
x : (i : ι) → π i
y : (i : { x // x ∈ t }) → π ↑i
i : { x // x ∈ s }
⊢ s.restrict (updateFinset x t y) i = restrict₂ hst y i

Tactic:
simp [updateFinset, dif_pos (hst i.2)]

Result:
no goals

Proof state:
ι : Type u_1
π : ι → Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
hst : s ⊆ t
x : (i : ι) → π i
y : (i : { x // x ∈ t }) → π ↑i
⊢ s.restrict (updateFinset x t y) = restrict₂ hst y

Tactic:
ext i

Result:
case h
ι : Type u_1
π : ι → Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
hst : s ⊆ t
x : (i : ι) → π i
y : (i : { x // x ∈ t }) → π ↑i
i : { x // x ∈ s }
⊢ s.restrict (updateFinset x t y) i = restrict₂ hst y i
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem IsMultiplicative.prodPrimeFactors_one_sub_of_squarefree [CommRing R]
    (f : ArithmeticFunction R) (hf : f.IsMultiplicative) {n : ℕ} (hn : Squarefree n) :
    ∏ p ∈ n.primeFactors, (1 - f p) = ∑ d ∈ n.divisors, μ d * f d

Proof state:
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 + ((↑μ).pmul f) p) = ∑ d ∈ n.divisors, ↑(μ d) * f d

Tactic:
rw [(isMultiplicative_moebius.intCast.pmul hf).prodPrimeFactors_one_add_of_squarefree hn]

Result:
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∑ d ∈ n.divisors, ((↑μ).pmul f) d = ∑ d ∈ n.divisors, ↑(μ d) * f d

Proof state:
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∀ x ∈ n.primeFactors, 1 - f x = 1 + ((↑μ).pmul f) x

Tactic:
intro p hp

Result:
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
p : ℕ
hp : p ∈ n.primeFactors
⊢ 1 - f p = 1 + ((↑μ).pmul f) p

Proof state:
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
p : ℕ
hp : p ∈ n.primeFactors
⊢ 1 - f p = 1 + ((↑μ).pmul f) p

Tactic:
rw [pmul_apply, intCoe_apply, ArithmeticFunction.moebius_apply_prime
    (prime_of_mem_primeFactorsList (List.mem_toFinset.mp hp))]

Result:
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
p : ℕ
hp : p ∈ n.primeFactors
⊢ 1 - f p = 1 + ↑(-1) * f p

Proof state:
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 - f p) = ∏ p ∈ n.primeFactors, (1 + ((↑μ).pmul f) p)

Tactic:
apply Finset.prod_congr rfl

Result:
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∀ x ∈ n.primeFactors, 1 - f x = 1 + ((↑μ).pmul f) x

Proof state:
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 - f p) = ∑ d ∈ n.divisors, ↑(μ d) * f d

Tactic:
trans (∏ p ∈ n.primeFactors, (1 + (ArithmeticFunction.pmul (μ : ArithmeticFunction R) f) p))

Result:
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 - f p) = ∏ p ∈ n.primeFactors, (1 + ((↑μ).pmul f) p)

R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 + ((↑μ).pmul f) p) = ∑ d ∈ n.divisors, ↑(μ d) * f d

Proof state:
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
p : ℕ
hp : p ∈ n.primeFactors
⊢ 1 - f p = 1 + ↑(-1) * f p

Tactic:
ring

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∑ d ∈ n.divisors, ((↑μ).pmul f) d = ∑ d ∈ n.divisors, ↑(μ d) * f d

Tactic:
simp_rw [pmul_apply, intCoe_apply]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem wf_isOption : WellFounded IsOption :=
  ⟨fun x =>
    moveRecOn x fun x IHl IHr =>
      Acc.intro x fun y h => by
        induction h with
        | moveLeft i => exact IHl i
        | moveRight j => exact IHr j⟩

Proof state:
case moveLeft
x✝¹ x y x✝ : PGame
i : x✝.LeftMoves
IHl : ∀ (i : x✝.LeftMoves), Acc IsOption (x✝.moveLeft i)
IHr : ∀ (j : x✝.RightMoves), Acc IsOption (x✝.moveRight j)
⊢ Acc IsOption (x✝.moveLeft i)

Tactic:
exact IHl i

Result:
no goals

Proof state:
case moveRight
x✝¹ x y x✝ : PGame
j : x✝.RightMoves
IHl : ∀ (i : x✝.LeftMoves), Acc IsOption (x✝.moveLeft i)
IHr : ∀ (j : x✝.RightMoves), Acc IsOption (x✝.moveRight j)
⊢ Acc IsOption (x✝.moveRight j)

Tactic:
exact IHr j

Result:
no goals

Proof state:
x✝ x : PGame
IHl : ∀ (i : x.LeftMoves), Acc IsOption (x.moveLeft i)
IHr : ∀ (j : x.RightMoves), Acc IsOption (x.moveRight j)
y : PGame
h : y.IsOption x
⊢ Acc IsOption y

Tactic:
induction h with
| moveLeft i => exact IHl i
| moveRight j => exact IHr j

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem star_eq_self {c₁ c₂ : R} {a : ℍ[R,c₁,c₂,c₃]} : star a = a ↔ a = a.re

Proof state:
R : Type u_3
c₃ : R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
c₁ c₂ : R
a : ℍ[R,c₁,c₂,c₃]
⊢ star a = a ↔ a = ↑a.re

Tactic:
simp_all [QuaternionAlgebra.ext_iff, neg_eq_iff_add_eq_zero, add_self_eq_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem getElem_zero_filter (p : α → Bool) (l : Array α) (h) :
    (l.filter p)[0] =
      (l.find? p).get (by cases l; simpa [← List.countP_eq_length_filter] using h)

Proof state:
α : Type u_1
p : α → Bool
l : Array α
h : 0 < (filter p l).size
⊢ (filter p l)[0] = (find? p l).get ⋯

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
h : 0 < (filter p { toList := toList✝ }).size
⊢ (filter p { toList := toList✝ })[0] = (find? p { toList := toList✝ }).get ⋯

Proof state:
α : Type ?u.29729
p : α → Bool
l : Array α
h : 0 < (filter p l).size
⊢ (find? p l).isSome = true

Tactic:
cases l

Result:
case mk
α : Type ?u.29729
p : α → Bool
toList✝ : List α
h : 0 < (filter p { toList := toList✝ }).size
⊢ (find? p { toList := toList✝ }).isSome = true

Proof state:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
h : 0 < (filter p { toList := toList✝ }).size
⊢ (filter p { toList := toList✝ })[0] = (find? p { toList := toList✝ }).get ⋯

Tactic:
simp [List.getElem_zero_eq_head]

Result:
no goals

Proof state:
case mk
α : Type ?u.29729
p : α → Bool
toList✝ : List α
h : 0 < (filter p { toList := toList✝ }).size
⊢ (find? p { toList := toList✝ }).isSome = true

Tactic:
simpa [← List.countP_eq_length_filter] using h

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
theorem isOpen [CompleteSpace E] : IsOpen (range ((↑) : (E ≃L[𝕜] F) → E →L[𝕜] F))

Proof state:
case h.e'_3.h.mpr.intro
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f
h_O : Continuous O
f' : E →L[𝕜] F
w : (E →L[𝕜] E)ˣ
hw : ↑w = O f'
⊢ f' ∈ range toContinuousLinearMap

Tactic:
use (unitsEquiv 𝕜 E w).trans e

Result:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f
h_O : Continuous O
f' : E →L[𝕜] F
w : (E →L[𝕜] E)ˣ
hw : ↑w = O f'
⊢ ↑(((unitsEquiv 𝕜 E) w).trans e) = f'

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
⊢ IsOpen (range toContinuousLinearMap)

Tactic:
rw [isOpen_iff_mem_nhds, forall_mem_range]

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
⊢ ∀ (i : E ≃L[𝕜] F), range toContinuousLinearMap ∈ 𝓝 ↑i

Proof state:
case h.e'_3.h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f
h_O : Continuous O
f' : E →L[𝕜] F
⊢ f' ∈ range toContinuousLinearMap ↔ f' ∈ O ⁻¹' {x | IsUnit x}

Tactic:
constructor

Result:
case h.e'_3.h.mp
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f
h_O : Continuous O
f' : E →L[𝕜] F
⊢ f' ∈ range toContinuousLinearMap → f' ∈ O ⁻¹' {x | IsUnit x}

case h.e'_3.h.mpr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f
h_O : Continuous O
f' : E →L[𝕜] F
⊢ f' ∈ O ⁻¹' {x | IsUnit x} → f' ∈ range toContinuousLinearMap
-- Mathlib/Control/Monad/Cont.lean
theorem WriterT.goto_mkLabel {α β ω : Type _} [EmptyCollection ω] (x : Label (α × ω) m β) (i : α) :
    goto (WriterT.mkLabel x) i = monadLift (goto x (i, ∅))

Proof state:
case mk
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : EmptyCollection ω
i : α
apply✝ : α × ω → m β
⊢ goto (mkLabel { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } (i, ∅))

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : EmptyCollection ω
x : Label (α × ω) m β
i : α
⊢ goto (mkLabel x) i = monadLift (goto x (i, ∅))

Tactic:
cases x

Result:
case mk
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : EmptyCollection ω
i : α
apply✝ : α × ω → m β
⊢ goto (mkLabel { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } (i, ∅))
-- Mathlib/NumberTheory/NumberField/FinitePlaces.lean
theorem maximalIdeal_mk (v : HeightOneSpectrum (𝓞 K)) : maximalIdeal (mk v) = v

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
⊢ (mk v).maximalIdeal = v

Tactic:
rw [← mk_eq_iff, mk_maximalIdeal]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/LevelOne.lean
lemma ModularForm.levelOne_weight_zero_rank_one : Module.rank ℂ (ModularForm Γ(1) 0) = 1

Proof state:
case intro
g : ModularForm Γ(1) 0
c' : ℂ
hc' : ⇑g = Function.const ℍ c'
⊢ ∃ c, c • const 1 = g

Tactic:
aesop

Result:
no goals

Proof state:
⊢ Module.rank ℂ (ModularForm Γ(1) 0) = 1

Tactic:
refine rank_eq_one (const 1) (by simp [DFunLike.ne_iff]) fun g ↦ ?_

Result:
g : ModularForm Γ(1) 0
⊢ ∃ c, c • const 1 = g

Proof state:
⊢ const 1 ≠ 0

Tactic:
simp [DFunLike.ne_iff]

Result:
no goals

Proof state:
g : ModularForm Γ(1) 0
⊢ ∃ c, c • const 1 = g

Tactic:
obtain ⟨c', hc'⟩ := levelOne_weight_zero_const g

Result:
case intro
g : ModularForm Γ(1) 0
c' : ℂ
hc' : ⇑g = Function.const ℍ c'
⊢ ∃ c, c • const 1 = g
-- Mathlib/GroupTheory/Congruence/BigOperators.lean
theorem multiset_prod {ι M : Type*} [CommMonoid M] (c : Con M) {s : Multiset ι}
    {f g : ι → M} (h : ∀ x ∈ s, c (f x) (g x)) :
    c (s.map f).prod (s.map g).prod

Proof state:
ι : Type u_1
M : Type u_2
inst✝ : CommMonoid M
c : Con M
s : Multiset ι
f g : ι → M
h : ∀ x ∈ s, c (f x) (g x)
⊢ c (Multiset.map f s).prod (Multiset.map g s).prod

Tactic:
rcases s

Result:
case mk
ι : Type u_1
M : Type u_2
inst✝ : CommMonoid M
c : Con M
s : Multiset ι
f g : ι → M
a✝ : List ι
h : ∀ x ∈ Quot.mk (⇑(List.isSetoid ι)) a✝, c (f x) (g x)
⊢ c (Multiset.map f (Quot.mk (⇑(List.isSetoid ι)) a✝)).prod (Multiset.map g (Quot.mk (⇑(List.isSetoid ι)) a✝)).prod

Proof state:
case mk
ι : Type u_1
M : Type u_2
inst✝ : CommMonoid M
c : Con M
s : Multiset ι
f g : ι → M
a✝ : List ι
h : ∀ x ∈ Quot.mk (⇑(List.isSetoid ι)) a✝, c (f x) (g x)
⊢ c (Multiset.map f (Quot.mk (⇑(List.isSetoid ι)) a✝)).prod (Multiset.map g (Quot.mk (⇑(List.isSetoid ι)) a✝)).prod

Tactic:
simpa using c.list_prod h

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem piecewise_compl {s : Set α} (hs : MeasurableSet sᶜ) (f g : α →ₛ β) :
    piecewise sᶜ hs f g = piecewise s hs.of_compl g f :=
  coe_injective <| by simp [hs]

Proof state:
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet sᶜ
f g : α →ₛ β
⊢ ⇑(piecewise sᶜ hs f g) = ⇑(piecewise s ⋯ g f)

Tactic:
simp [hs]

Result:
no goals