harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/WittVector/Domain.lean
theorem verschiebung_shift (x : 𝕎 R) (k : ℕ) (h : ∀ i < k + 1, x.coeff i = 0) :
    verschiebung (x.shift k.succ) = x.shift k

Proof state:
case h.zero.a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ i < k + 1, x.coeff i = 0
⊢ k + 0 < k + 1

Tactic:
apply Nat.lt_succ_self

Result:
no goals

Proof state:
case h.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ i < k + 1, x.coeff i = 0
n✝ : ℕ
⊢ x.coeff (k.succ + n✝) = x.coeff (k + (n✝ + 1))

Tactic:
congr 1

Result:
case h.succ.e_a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ i < k + 1, x.coeff i = 0
n✝ : ℕ
⊢ k.succ + n✝ = k + (n✝ + 1)

Proof state:
case h.zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ i < k + 1, x.coeff i = 0
⊢ (verschiebung (x.shift k.succ)).coeff 0 = (x.shift k).coeff 0

Tactic:
rw [verschiebung_coeff_zero, shift_coeff, h]

Result:
case h.zero.a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ i < k + 1, x.coeff i = 0
⊢ k + 0 < k + 1

Proof state:
case h.succ.e_a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ i < k + 1, x.coeff i = 0
n✝ : ℕ
⊢ k.succ + n✝ = k + (n✝ + 1)

Tactic:
rw [Nat.add_succ, add_comm, Nat.add_succ, add_comm]

Result:
no goals

Proof state:
case h.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ i < k + 1, x.coeff i = 0
n✝ : ℕ
⊢ (verschiebung (x.shift k.succ)).coeff (n✝ + 1) = (x.shift k).coeff (n✝ + 1)

Tactic:
simp only [verschiebung_coeff_succ, shift]

Result:
case h.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ i < k + 1, x.coeff i = 0
n✝ : ℕ
⊢ x.coeff (k.succ + n✝) = x.coeff (k + (n✝ + 1))

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ i < k + 1, x.coeff i = 0
⊢ verschiebung (x.shift k.succ) = x.shift k

Tactic:
ext ⟨j⟩

Result:
case h.zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ i < k + 1, x.coeff i = 0
⊢ (verschiebung (x.shift k.succ)).coeff 0 = (x.shift k).coeff 0

case h.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ i < k + 1, x.coeff i = 0
n✝ : ℕ
⊢ (verschiebung (x.shift k.succ)).coeff (n✝ + 1) = (x.shift k).coeff (n✝ + 1)
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem chromaticNumber_le_of_forall_imp {V' : Type*} {G' : SimpleGraph V'}
    (h : ∀ n, G'.Colorable n → G.Colorable n) :
    G.chromaticNumber ≤ G'.chromaticNumber

Proof state:
V : Type u
G : SimpleGraph V
V' : Type u_3
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
m : ℕ
hc : G'.Colorable m
this : G.Colorable m
⊢ ⨅ n, ⨅ (_ : G.Colorable n), ↑n ≤ ↑m

Tactic:
rw [← chromaticNumber_le_iff_colorable] at this

Result:
V : Type u
G : SimpleGraph V
V' : Type u_3
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
m : ℕ
hc : G'.Colorable m
this : G.chromaticNumber ≤ ↑m
⊢ ⨅ n, ⨅ (_ : G.Colorable n), ↑n ≤ ↑m

Proof state:
V : Type u
G : SimpleGraph V
V' : Type u_3
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
m : ℕ
hc : G'.Colorable m
this : G.chromaticNumber ≤ ↑m
⊢ ⨅ n, ⨅ (_ : G.Colorable n), ↑n ≤ ↑m

Tactic:
exact this

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
V' : Type u_3
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
⊢ ∀ (i : ℕ), G'.Colorable i → ⨅ n, ⨅ (_ : G.Colorable n), ↑n ≤ ↑i

Tactic:
intro m hc

Result:
V : Type u
G : SimpleGraph V
V' : Type u_3
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
m : ℕ
hc : G'.Colorable m
⊢ ⨅ n, ⨅ (_ : G.Colorable n), ↑n ≤ ↑m

Proof state:
V : Type u
G : SimpleGraph V
V' : Type u_3
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
⊢ ⨅ n ∈ setOf G.Colorable, ↑n ≤ ⨅ n ∈ setOf G'.Colorable, ↑n

Tactic:
simp only [Set.mem_setOf_eq, le_iInf_iff]

Result:
V : Type u
G : SimpleGraph V
V' : Type u_3
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
⊢ ∀ (i : ℕ), G'.Colorable i → ⨅ n, ⨅ (_ : G.Colorable n), ↑n ≤ ↑i

Proof state:
V : Type u
G : SimpleGraph V
V' : Type u_3
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
m : ℕ
hc : G'.Colorable m
⊢ ⨅ n, ⨅ (_ : G.Colorable n), ↑n ≤ ↑m

Tactic:
have := h _ hc

Result:
V : Type u
G : SimpleGraph V
V' : Type u_3
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
m : ℕ
hc : G'.Colorable m
this : G.Colorable m
⊢ ⨅ n, ⨅ (_ : G.Colorable n), ↑n ≤ ↑m

Proof state:
V : Type u
G : SimpleGraph V
V' : Type u_3
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
⊢ G.chromaticNumber ≤ G'.chromaticNumber

Tactic:
rw [chromaticNumber, chromaticNumber]

Result:
V : Type u
G : SimpleGraph V
V' : Type u_3
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
⊢ ⨅ n ∈ setOf G.Colorable, ↑n ≤ ⨅ n ∈ setOf G'.Colorable, ↑n
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lt_add_iff {a b c : Ordinal} (hc : c ≠ 0) : a < b + c ↔ ∃ d < c, a ≤ b + d

Proof state:
case mpr.intro.intro
a b c : Ordinal.{u_4}
hc : c ≠ 0
d : Ordinal.{u_4}
hd : d < c
ha : a ≤ b + d
⊢ a < b + c

Tactic:
exact ha.trans_lt (add_lt_add_left hd b)

Result:
no goals

Proof state:
a b c : Ordinal.{u_4}
hc : c ≠ 0
⊢ a < b + c ↔ ∃ d < c, a ≤ b + d

Tactic:
use fun h ↦ ⟨_, sub_lt_of_lt_add h hc.bot_lt, le_add_sub a b⟩

Result:
case mpr
a b c : Ordinal.{u_4}
hc : c ≠ 0
⊢ (∃ d < c, a ≤ b + d) → a < b + c

Proof state:
case mpr
a b c : Ordinal.{u_4}
hc : c ≠ 0
⊢ (∃ d < c, a ≤ b + d) → a < b + c

Tactic:
rintro ⟨d, hd, ha⟩

Result:
case mpr.intro.intro
a b c : Ordinal.{u_4}
hc : c ≠ 0
d : Ordinal.{u_4}
hd : d < c
ha : a ≤ b + d
⊢ a < b + c
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem ne_one_of_norm_ne_zero : ‖a‖ ≠ 0 → a ≠ 1 :=
  mt <| by
    rintro rfl
    exact norm_one'

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
⊢ ‖1‖ = 0

Tactic:
exact norm_one'

Result:
no goals

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ a = 1 → ‖a‖ = 0

Tactic:
rintro rfl

Result:
E : Type u_5
inst✝ : SeminormedGroup E
⊢ ‖1‖ = 0
-- Mathlib/Algebra/Module/Presentation/Free.lean
lemma free_iff_exists_presentation :
    Free A M ↔ ∃ (p : Presentation.{v, w₁} A M), IsEmpty p.R

Proof state:
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
G : Type v
e : M ≃ₗ[A] G →₀ A
⊢ IsEmpty PEmpty.{w₁ + 1}

Tactic:
infer_instance

Result:
no goals

Proof state:
case mp
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ (∃ I, Nonempty (Basis I A M)) → ∃ p, IsEmpty p.R

Tactic:
rintro ⟨G, ⟨⟨e⟩⟩⟩

Result:
case mp.intro.intro.ofRepr
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
G : Type v
e : M ≃ₗ[A] G →₀ A
⊢ ∃ p, IsEmpty p.R

Proof state:
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
G : Type v
e : M ≃ₗ[A] G →₀ A
⊢ IsEmpty ((presentationFinsupp A G).ofLinearEquiv e.symm).R

Tactic:
dsimp

Result:
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
G : Type v
e : M ≃ₗ[A] G →₀ A
⊢ IsEmpty PEmpty.{w₁ + 1}

Proof state:
case mpr
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ (∃ p, IsEmpty p.R) → Free A M

Tactic:
rintro ⟨p, h⟩

Result:
case mpr.intro
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
p : Presentation A M
h : IsEmpty p.R
⊢ Free A M

Proof state:
case mpr.intro
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
p : Presentation A M
h : IsEmpty p.R
⊢ Free A M

Tactic:
exact p.toIsPresentation.free

Result:
no goals

Proof state:
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ Free A M ↔ ∃ p, IsEmpty p.R

Tactic:
constructor

Result:
case mp
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ Free A M → ∃ p, IsEmpty p.R

case mpr
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ (∃ p, IsEmpty p.R) → Free A M

Proof state:
case mp
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ Free A M → ∃ p, IsEmpty p.R

Tactic:
rw [free_def.{_, _, v}]

Result:
case mp
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ (∃ I, Nonempty (Basis I A M)) → ∃ p, IsEmpty p.R

Proof state:
case mp.intro.intro.ofRepr
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
G : Type v
e : M ≃ₗ[A] G →₀ A
⊢ ∃ p, IsEmpty p.R

Tactic:
exact ⟨(presentationFinsupp A G).ofLinearEquiv e.symm,
  by dsimp; infer_instance⟩

Result:
no goals
-- Mathlib/RingTheory/Localization/BaseChange.lean
theorem tensorProduct_compatibleSMul : CompatibleSMul R A M₁ M₂ where
  smul_tmul a _ _

Proof state:
R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
inst✝¹ : IsScalarTower R A M₁
inst✝ : IsScalarTower R A M₂
a : A
x✝¹ : M₁
x✝ : M₂
⊢ (a • x✝¹) ⊗ₜ[R] x✝ = x✝¹ ⊗ₜ[R] (a • x✝)

Tactic:
obtain ⟨r, s, rfl⟩ := mk'_surjective S a

Result:
case intro.intro
R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
inst✝¹ : IsScalarTower R A M₁
inst✝ : IsScalarTower R A M₂
x✝¹ : M₁
x✝ : M₂
r : R
s : ↥S
⊢ (mk' A r s • x✝¹) ⊗ₜ[R] x✝ = x✝¹ ⊗ₜ[R] (mk' A r s • x✝)

Proof state:
case intro.intro
R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
inst✝¹ : IsScalarTower R A M₁
inst✝ : IsScalarTower R A M₂
x✝¹ : M₁
x✝ : M₂
r : R
s : ↥S
⊢ (mk' A r s • x✝¹) ⊗ₜ[R] x✝ = x✝¹ ⊗ₜ[R] (mk' A r s • x✝)

Tactic:
rw [← (map_units A s).smul_left_cancel]

Result:
case intro.intro
R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
inst✝¹ : IsScalarTower R A M₁
inst✝ : IsScalarTower R A M₂
x✝¹ : M₁
x✝ : M₂
r : R
s : ↥S
⊢ (algebraMap R A) ↑s • (mk' A r s • x✝¹) ⊗ₜ[R] x✝ = (algebraMap R A) ↑s • x✝¹ ⊗ₜ[R] (mk' A r s • x✝)

Proof state:
case intro.intro
R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
inst✝¹ : IsScalarTower R A M₁
inst✝ : IsScalarTower R A M₂
x✝¹ : M₁
x✝ : M₂
r : R
s : ↥S
⊢ (algebraMap R A) ↑s • (mk' A r s • x✝¹) ⊗ₜ[R] x✝ = (algebraMap R A) ↑s • x✝¹ ⊗ₜ[R] (mk' A r s • x✝)

Tactic:
simp_rw [algebraMap_smul, smul_tmul', ← smul_assoc, smul_tmul, ← smul_assoc, smul_mk'_self,
  algebraMap_smul, smul_tmul]

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
lemma nat_repr_len_aux (n b e : Nat) (h_b_pos : 0 < b) :  n < b ^ e.succ → n / b < b ^ e

Proof state:
n b e : ℕ
h_b_pos : 0 < b
⊢ n < b ^ e.succ → n / b < b ^ e

Tactic:
simp only [Nat.pow_succ]

Result:
n b e : ℕ
h_b_pos : 0 < b
⊢ n < b ^ e * b → n / b < b ^ e

Proof state:
n b e : ℕ
h_b_pos : 0 < b
⊢ n < b ^ e * b → n / b < b ^ e

Tactic:
exact (@Nat.div_lt_iff_lt_mul b n (b ^ e) h_b_pos).mpr

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem deriv_add_eq_mul_omega0_add (a b : Ordinal.{u}) : deriv (a + ·) b = a * ω + b

Proof state:
case refine_2
a✝ a : Ordinal.{u}
h : deriv (fun x => a✝ + x) a = a✝ * ω + a
⊢ nfp (fun x => a✝ + x) (succ (a✝ * ω + a)) = succ (a✝ * ω + a)

Tactic:
exact nfp_eq_self (add_eq_right_iff_mul_omega0_le.2 ((le_add_right _ _).trans (le_succ _)))

Result:
no goals

Proof state:
case refine_2
a✝ a : Ordinal.{u}
h : deriv (fun x => a✝ + x) a = a✝ * ω + a
⊢ deriv (fun x => a✝ + x) (succ a) = a✝ * ω + succ a

Tactic:
rw [deriv_succ, h, add_succ]

Result:
case refine_2
a✝ a : Ordinal.{u}
h : deriv (fun x => a✝ + x) a = a✝ * ω + a
⊢ nfp (fun x => a✝ + x) (succ (a✝ * ω + a)) = succ (a✝ * ω + a)

Proof state:
case refine_1
a : Ordinal.{u}
⊢ nfp (fun x => a + x) 0 = a * ω

Tactic:
exact nfp_add_zero a

Result:
no goals

Proof state:
a : Ordinal.{u}
⊢ deriv (fun x => a + x) 0 = a * ω + 0 ∧
    ∀ (a_1 : Ordinal.{u}),
      deriv (fun x => a + x) a_1 = a * ω + a_1 → deriv (fun x => a + x) (succ a_1) = a * ω + succ a_1

Tactic:
refine ⟨?_, fun a h => ?_⟩

Result:
case refine_1
a : Ordinal.{u}
⊢ deriv (fun x => a + x) 0 = a * ω + 0

case refine_2
a✝ a : Ordinal.{u}
h : deriv (fun x => a✝ + x) a = a✝ * ω + a
⊢ deriv (fun x => a✝ + x) (succ a) = a✝ * ω + succ a

Proof state:
case refine_1
a : Ordinal.{u}
⊢ deriv (fun x => a + x) 0 = a * ω + 0

Tactic:
rw [deriv_zero_right, add_zero]

Result:
case refine_1
a : Ordinal.{u}
⊢ nfp (fun x => a + x) 0 = a * ω

Proof state:
a : Ordinal.{u}
⊢ ∀ (b : Ordinal.{u}), deriv (fun x => a + x) b = a * ω + b

Tactic:
rw [← funext_iff, IsNormal.eq_iff_zero_and_succ (isNormal_deriv _) (isNormal_add_right _)]

Result:
a : Ordinal.{u}
⊢ deriv (fun x => a + x) 0 = a * ω + 0 ∧
    ∀ (a_1 : Ordinal.{u}),
      deriv (fun x => a + x) a_1 = a * ω + a_1 → deriv (fun x => a + x) (succ a_1) = a * ω + succ a_1

Proof state:
a b : Ordinal.{u}
⊢ deriv (fun x => a + x) b = a * ω + b

Tactic:
revert b

Result:
a : Ordinal.{u}
⊢ ∀ (b : Ordinal.{u}), deriv (fun x => a + x) b = a * ω + b
-- Mathlib/Data/Finsupp/Defs.lean
theorem unique_ext [Unique α] {f g : α →₀ M} (h : f default = g default) : f = g :=
  ext fun a => by rwa [Unique.eq_default a]

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : Unique α
f g : α →₀ M
h : f default = g default
a : α
⊢ f a = g a

Tactic:
rwa [Unique.eq_default a]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem irreducible_mk {a : M} : Irreducible (Associates.mk a) ↔ Irreducible a

Proof state:
case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ (∀ (a_1 b : M), a = a_1 * b → IsUnit a_1 ∨ IsUnit b) → ∀ (a_2 a_3 : M), a_2 * a_3 ~ᵤ a → IsUnit a_2 ∨ IsUnit a_3

Tactic:
rintro h x y ⟨u, rfl⟩

Result:
case mpr.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
x y : M
u : Mˣ
h : ∀ (a b : M), x * y * ↑u = a * b → IsUnit a ∨ IsUnit b
⊢ IsUnit x ∨ IsUnit y

Proof state:
case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ (∀ (a_1 a_2 : M), a_1 * a_2 ~ᵤ a → IsUnit a_1 ∨ IsUnit a_2) → ∀ (a_2 b : M), a = a_2 * b → IsUnit a_2 ∨ IsUnit b

Tactic:
rintro h x y rfl

Result:
case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
x y : M
h : ∀ (a a_1 : M), a * a_1 ~ᵤ x * y → IsUnit a ∨ IsUnit a_1
⊢ IsUnit x ∨ IsUnit y

Proof state:
M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ (¬IsUnit a ∧ ∀ (a_1 a_2 : M), a_1 * a_2 ~ᵤ a → IsUnit a_1 ∨ IsUnit a_2) ↔
    ¬IsUnit a ∧ ∀ (a_1 b : M), a = a_1 * b → IsUnit a_1 ∨ IsUnit b

Tactic:
apply Iff.rfl.and

Result:
M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ (∀ (a_1 a_2 : M), a_1 * a_2 ~ᵤ a → IsUnit a_1 ∨ IsUnit a_2) ↔ ∀ (a_1 b : M), a = a_1 * b → IsUnit a_1 ∨ IsUnit b

Proof state:
M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ (∀ (a_1 a_2 : M), a_1 * a_2 ~ᵤ a → IsUnit a_1 ∨ IsUnit a_2) ↔ ∀ (a_1 b : M), a = a_1 * b → IsUnit a_1 ∨ IsUnit b

Tactic:
constructor

Result:
case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ (∀ (a_1 a_2 : M), a_1 * a_2 ~ᵤ a → IsUnit a_1 ∨ IsUnit a_2) → ∀ (a_2 b : M), a = a_2 * b → IsUnit a_2 ∨ IsUnit b

case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ (∀ (a_1 b : M), a = a_1 * b → IsUnit a_1 ∨ IsUnit b) → ∀ (a_2 a_3 : M), a_2 * a_3 ~ᵤ a → IsUnit a_2 ∨ IsUnit a_3

Proof state:
case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
x y : M
h : ∀ (a a_1 : M), a * a_1 ~ᵤ x * y → IsUnit a ∨ IsUnit a_1
⊢ IsUnit x ∨ IsUnit y

Tactic:
exact h _ _ <| .refl _

Result:
no goals

Proof state:
case mpr.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
x y : M
u : Mˣ
h : ∀ (a b : M), x * y * ↑u = a * b → IsUnit a ∨ IsUnit b
⊢ IsUnit x ∨ IsUnit y

Tactic:
simpa using h x (y * u) (mul_assoc _ _ _)

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ Irreducible (Associates.mk a) ↔ Irreducible a

Tactic:
simp only [irreducible_iff, isUnit_mk, forall_associated, isUnit_mk, mk_mul_mk,
  mk_eq_mk_iff_associated, Associated.comm (x := a)]

Result:
M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ (¬IsUnit a ∧ ∀ (a_1 a_2 : M), a_1 * a_2 ~ᵤ a → IsUnit a_1 ∨ IsUnit a_2) ↔
    ¬IsUnit a ∧ ∀ (a_1 b : M), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_insert [LawfulBEq α] (h : m.WF) {k a : α} {v : β k} {h₁} :
    (m.insert k v).get a h₁ =
      if h₂ : k == a then
        cast (congrArg β (eq_of_beq h₂)) v
      else
        m.get a (mem_of_mem_insert h h₁ (Bool.eq_false_iff.2 h₂))

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
k a : α
v : β k
h₁ : a ∈ m.insert k v
⊢ (m.insert k v).get a h₁ = if h₂ : (k == a) = true then cast ⋯ v else m.get a ⋯

Tactic:
simp_to_raw using Raw₀.get_insert ⟨m, _⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem and_congr_right_iff : (a ∧ b ↔ a ∧ c) ↔ (a → (b ↔ c)) :=
  Iff.intro (fun h ha => by simp [ha] at h; exact h) and_congr_right

Proof state:
a b c : Prop
ha : a
h : b ↔ c
⊢ b ↔ c

Tactic:
exact h

Result:
no goals

Proof state:
a b c : Prop
h : a ∧ b ↔ a ∧ c
ha : a
⊢ b ↔ c

Tactic:
simp [ha] at h

Result:
a b c : Prop
ha : a
h : b ↔ c
⊢ b ↔ c
-- Mathlib/Data/Matrix/Basic.lean
theorem map_algebraMap (r : R) (f : α → β) (hf : f 0 = 0)
    (hf₂ : f (algebraMap R α r) = algebraMap R β r) :
    (algebraMap R (Matrix n n α) r).map f = algebraMap R (Matrix n n β) r

Proof state:
n : Type u_3
R : Type u_7
α : Type v
β : Type w
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f ((algebraMap R α) r) = (algebraMap R β) r
⊢ n → f ((algebraMap R α) r) = (algebraMap R β) r

Tactic:
intro

Result:
n : Type u_3
R : Type u_7
α : Type v
β : Type w
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f ((algebraMap R α) r) = (algebraMap R β) r
i✝ : n
⊢ f ((algebraMap R α) r) = (algebraMap R β) r

Proof state:
n : Type u_3
R : Type u_7
α : Type v
β : Type w
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f ((algebraMap R α) r) = (algebraMap R β) r
i✝ : n
⊢ f ((algebraMap R α) r) = (algebraMap R β) r

Tactic:
rw [hf₂]

Result:
no goals

Proof state:
n : Type u_3
R : Type u_7
α : Type v
β : Type w
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f ((algebraMap R α) r) = (algebraMap R β) r
⊢ ((algebraMap R (Matrix n n α)) r).map f = (algebraMap R (Matrix n n β)) r

Tactic:
rw [algebraMap_eq_diagonal, algebraMap_eq_diagonal, diagonal_map hf]

Result:
n : Type u_3
R : Type u_7
α : Type v
β : Type w
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f ((algebraMap R α) r) = (algebraMap R β) r
⊢ (diagonal fun m => f ((algebraMap R (n → α)) r m)) = diagonal ((algebraMap R (n → β)) r)

Proof state:
n : Type u_3
R : Type u_7
α : Type v
β : Type w
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f ((algebraMap R α) r) = (algebraMap R β) r
⊢ (diagonal fun m => f ((algebraMap R (n → α)) r m)) = diagonal ((algebraMap R (n → β)) r)

Tactic:
simp only [Pi.algebraMap_apply, diagonal_eq_diagonal_iff]

Result:
n : Type u_3
R : Type u_7
α : Type v
β : Type w
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f ((algebraMap R α) r) = (algebraMap R β) r
⊢ n → f ((algebraMap R α) r) = (algebraMap R β) r
-- Mathlib/Order/LiminfLimsup.lean
theorem isCobounded_bot : IsCobounded r ⊥ ↔ ∃ b, ∀ x, r b x

Proof state:
α : Type u_1
r : α → α → Prop
⊢ IsCobounded r ⊥ ↔ ∃ b, ∀ (x : α), r b x

Tactic:
simp [IsCobounded]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem precomp_uniformContinuous {𝔗 : Set (Set γ)} {f : γ → α}
    (hf : MapsTo (f '' ·) 𝔗 𝔖) :
    UniformContinuous fun g : α →ᵤ[𝔖] β => ofFun 𝔗 (toFun 𝔖 g ∘ f)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : MapsTo (fun x => f '' x) 𝔗 𝔖
t : Set γ
ht : t ∈ 𝔗
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ Tendsto (fun x => ((ofFun 𝔗) ((toFun 𝔖) x.1 ∘ f), (ofFun 𝔗) ((toFun 𝔖) x.2 ∘ f))) (𝓟 (UniformOnFun.gen 𝔖 (f '' t) V))
    (𝓟 (UniformOnFun.gen 𝔗 t V))

Tactic:
simpa only [tendsto_principal_principal, UniformOnFun.gen] using fun _ ↦ forall_mem_image.1

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : MapsTo (fun x => f '' x) 𝔗 𝔖
⊢ UniformContinuous fun g => (ofFun 𝔗) ((toFun 𝔖) g ∘ f)

Tactic:
simp_rw [UniformContinuous, UniformOnFun.uniformity_eq, tendsto_iInf]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : MapsTo (fun x => f '' x) 𝔗 𝔖
⊢ ∀ i ∈ 𝔗,
    ∀ i_2 ∈ 𝓤 β,
      Tendsto (fun x => ((ofFun 𝔗) ((toFun 𝔖) x.1 ∘ f), (ofFun 𝔗) ((toFun 𝔖) x.2 ∘ f)))
        (⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V)) (𝓟 (UniformOnFun.gen 𝔗 i i_2))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : MapsTo (fun x => f '' x) 𝔗 𝔖
⊢ ∀ i ∈ 𝔗,
    ∀ i_2 ∈ 𝓤 β,
      Tendsto (fun x => ((ofFun 𝔗) ((toFun 𝔖) x.1 ∘ f), (ofFun 𝔗) ((toFun 𝔖) x.2 ∘ f)))
        (⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V)) (𝓟 (UniformOnFun.gen 𝔗 i i_2))

Tactic:
refine fun t ht V hV ↦ tendsto_iInf' (f '' t) <| tendsto_iInf' (hf ht) <|
  tendsto_iInf' V <| tendsto_iInf' hV ?_

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : MapsTo (fun x => f '' x) 𝔗 𝔖
t : Set γ
ht : t ∈ 𝔗
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ Tendsto (fun x => ((ofFun 𝔗) ((toFun 𝔖) x.1 ∘ f), (ofFun 𝔗) ((toFun 𝔖) x.2 ∘ f))) (𝓟 (UniformOnFun.gen 𝔖 (f '' t) V))
    (𝓟 (UniformOnFun.gen 𝔗 t V))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pred_max_pred : ∀ (x y), max (pred x) (pred y) = pred (max x y)
  | 0, _ => by simp only [Nat.pred_zero, Nat.zero_max]
  | _, 0 => by simp only [Nat.pred_zero, Nat.max_zero]
  | _+1, _+1 => by simp only [Nat.pred_succ, Nat.succ_max_succ]

Proof state:
x✝ : Nat
⊢ max x✝.pred (pred 0) = (max x✝ 0).pred

Tactic:
simp only [Nat.pred_zero, Nat.max_zero]

Result:
no goals

Proof state:
n✝¹ n✝ : Nat
⊢ max (n✝¹ + 1).pred (n✝ + 1).pred = (max (n✝¹ + 1) (n✝ + 1)).pred

Tactic:
simp only [Nat.pred_succ, Nat.succ_max_succ]

Result:
no goals

Proof state:
x✝ : Nat
⊢ max (pred 0) x✝.pred = (max 0 x✝).pred

Tactic:
simp only [Nat.pred_zero, Nat.zero_max]

Result:
no goals