harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/ModelTheory/Algebra/Ring/FreeCommRing.lean
theorem realize_termOfFreeCommRing (p : FreeCommRing α) (v : α → R) :
    (termOfFreeCommRing p).realize v = FreeCommRing.lift v p

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
x✝ : CompatibleRing (FreeCommRing α) := compatibleRingOfRing (FreeCommRing α)
⊢ Term.realize v (Classical.choose ⋯) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (Classical.choose ⋯))

Tactic:
induction Classical.choose (exists_term_realize_eq_freeCommRing p) with
| var _ => simp
| func f a ih =>
  cases f <;>
  simp [ih]

Result:
no goals

Proof state:
case func
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
x✝ : CompatibleRing (FreeCommRing α) := compatibleRingOfRing (FreeCommRing α)
l✝ : ℕ
f : ring.Functions l✝
a : Fin l✝ → ring.Term α
ih : ∀ (a_1 : Fin l✝), Term.realize v (a a_1) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize v (func f a) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (func f a))

Tactic:
cases f <;>
simp [ih]

Result:
no goals

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
⊢ Term.realize v (termOfFreeCommRing p) = (FreeCommRing.lift v) p

Tactic:
let _ := compatibleRingOfRing (FreeCommRing α)

Result:
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
x✝ : CompatibleRing (FreeCommRing α) := compatibleRingOfRing (FreeCommRing α)
⊢ Term.realize v (termOfFreeCommRing p) = (FreeCommRing.lift v) p

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
x✝ : CompatibleRing (FreeCommRing α) := compatibleRingOfRing (FreeCommRing α)
⊢ Term.realize v (termOfFreeCommRing p) = (FreeCommRing.lift v) p

Tactic:
rw [termOfFreeCommRing]

Result:
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
x✝ : CompatibleRing (FreeCommRing α) := compatibleRingOfRing (FreeCommRing α)
⊢ Term.realize v (Classical.choose ⋯) = (FreeCommRing.lift v) p

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
x✝ : CompatibleRing (FreeCommRing α) := compatibleRingOfRing (FreeCommRing α)
⊢ Term.realize v (Classical.choose ⋯) = (FreeCommRing.lift v) p

Tactic:
conv_rhs => rw [← Classical.choose_spec (exists_term_realize_eq_freeCommRing p)]

Result:
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
x✝ : CompatibleRing (FreeCommRing α) := compatibleRingOfRing (FreeCommRing α)
⊢ Term.realize v (Classical.choose ⋯) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (Classical.choose ⋯))

Proof state:
case var
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
x✝ : CompatibleRing (FreeCommRing α) := compatibleRingOfRing (FreeCommRing α)
a✝ : α
⊢ Term.realize v (var a✝) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (var a✝))

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem mul_right_mono (I : FractionalIdeal S P) : Monotone fun J => J * I

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J J' : FractionalIdeal S P
h : J ≤ J'
⊢ (fun J => J * I) J ≤ (fun J => J * I) J'

Tactic:
simp only [mul_def]

Result:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J J' : FractionalIdeal S P
h : J ≤ J'
⊢ ⟨↑J * ↑I, ⋯⟩ ≤ ⟨↑J' * ↑I, ⋯⟩

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
⊢ Monotone fun J => J * I

Tactic:
intro J J' h

Result:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J J' : FractionalIdeal S P
h : J ≤ J'
⊢ (fun J => J * I) J ≤ (fun J => J * I) J'

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J J' : FractionalIdeal S P
h : J ≤ J'
⊢ ⟨↑J * ↑I, ⋯⟩ ≤ ⟨↑J' * ↑I, ⋯⟩

Tactic:
exact mul_le.mpr fun x hx y hy => mul_mem_mul (h hx) hy

Result:
no goals
-- Mathlib/NumberTheory/FLT/Four.lean
theorem not_minimal {a b c : ℤ} (h : Minimal a b c) (ha2 : a % 2 = 1) (hc : 0 < c) : False

Proof state:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : m.gcd (r * s) = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = m * (r * s)
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi : m = i ^ 2 ∨ m = -i ^ 2
h1 : m = -i ^ 2
⊢ False

Tactic:
have hit : -i ^ 2 ≤ 0 := neg_nonpos.mpr (sq_nonneg i)

Result:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : m.gcd (r * s) = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = m * (r * s)
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi : m = i ^ 2 ∨ m = -i ^ 2
h1 : m = -i ^ 2
hit : -i ^ 2 ≤ 0
⊢ False
-- Mathlib/Data/Nat/BitIndices.lean
theorem bitIndices_two_mul_add_one (n : ℕ) :
    bitIndices (2 * n + 1) = 0 :: (bitIndices n).map (· + 1)

Proof state:
n : ℕ
⊢ (2 * n + 1).bitIndices = 0 :: map (fun x => x + 1) n.bitIndices

Tactic:
rw [← bitIndices_bit_true, bit_true]

Result:
no goals
-- Mathlib/Topology/Algebra/Order/LiminfLimsup.lean
theorem tendsto_of_le_liminf_of_limsup_le {f : Filter β} {u : β → α} {a : α} (hinf : a ≤ liminf u f)
    (hsup : limsup u f ≤ a) (h : f.IsBoundedUnder (· ≤ ·) u

Proof state:
α : Type u_2
β : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : Filter β
u : β → α
a : α
hinf : a ≤ liminf u f
hsup : limsup u f ≤ a
h : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
⊢ Tendsto u f (𝓝 a)

Tactic:
rcases f.eq_or_neBot with rfl | _

Result:
case inl
α : Type u_2
β : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
u : β → α
a : α
hinf : a ≤ liminf u ⊥
hsup : limsup u ⊥ ≤ a
h : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) ⊥ u) _auto✝
h' : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) ⊥ u) _auto✝
⊢ Tendsto u ⊥ (𝓝 a)

case inr
α : Type u_2
β : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : Filter β
u : β → α
a : α
hinf : a ≤ liminf u f
hsup : limsup u f ≤ a
h : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
h✝ : f.NeBot
⊢ Tendsto u f (𝓝 a)

Proof state:
case inr
α : Type u_2
β : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : Filter β
u : β → α
a : α
hinf : a ≤ liminf u f
hsup : limsup u f ≤ a
h : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
h✝ : f.NeBot
⊢ Tendsto u f (𝓝 a)

Tactic:
exact tendsto_of_liminf_eq_limsup (le_antisymm (le_trans (liminf_le_limsup h h') hsup) hinf)
  (le_antisymm hsup (le_trans hinf (liminf_le_limsup h h'))) h h'

Result:
no goals

Proof state:
case inl
α : Type u_2
β : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
u : β → α
a : α
hinf : a ≤ liminf u ⊥
hsup : limsup u ⊥ ≤ a
h : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) ⊥ u) _auto✝
h' : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) ⊥ u) _auto✝
⊢ Tendsto u ⊥ (𝓝 a)

Tactic:
exact tendsto_bot

Result:
no goals
-- Mathlib/Algebra/Quandle.lean
theorem self_act_eq_iff_eq {x y : R} : x ◃ x = y ◃ y ↔ x = y

Proof state:
case mp
R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ x = y

Tactic:
trans (x ◃ x) ◃⁻¹ x ◃ x

Result:
R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ x = (x ◃ x) ◃⁻¹ x ◃ x

R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ (x ◃ x) ◃⁻¹ x ◃ x = y

Proof state:
case mp
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y → x = y

case mpr
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x = y → x ◃ x = y ◃ y

Tactic:
swap

Result:
case mpr
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x = y → x ◃ x = y ◃ y

case mp
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y → x = y

Proof state:
R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ x = (x ◃ x) ◃⁻¹ x ◃ x

Tactic:
rw [← left_cancel (x ◃ x), right_inv, self_act_act_eq]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y ↔ x = y

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y → x = y

case mpr
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x = y → x ◃ x = y ◃ y

Proof state:
case mpr
R : Type u_1
inst✝ : Rack R
x : R
⊢ x ◃ x = x ◃ x

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ (x ◃ x) ◃⁻¹ x ◃ x = y

Tactic:
rw [h, ← left_cancel (y ◃ y), right_inv, self_act_act_eq]

Result:
no goals

Proof state:
case mpr
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x = y → x ◃ x = y ◃ y

Tactic:
rintro rfl

Result:
case mpr
R : Type u_1
inst✝ : Rack R
x : R
⊢ x ◃ x = x ◃ x

Proof state:
case mp
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y → x = y

Tactic:
intro h

Result:
case mp
R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ x = y
-- Mathlib/Data/Nat/Choose/Factorization.lean
theorem factorization_choose_le_one (p_large : n < p ^ 2) : (choose n k).factorization p ≤ 1

Proof state:
case inl
p k : ℕ
p_large : 0 < p ^ 2
⊢ log p 0 ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
p n k : ℕ
p_large : n < p ^ 2
⊢ log p n ≤ 1

Tactic:
rcases eq_or_ne n 0 with (rfl | hn0)

Result:
case inl
p k : ℕ
p_large : 0 < p ^ 2
⊢ log p 0 ≤ 1

case inr
p n k : ℕ
p_large : n < p ^ 2
hn0 : n ≠ 0
⊢ log p n ≤ 1

Proof state:
p n k : ℕ
p_large : n < p ^ 2
⊢ (n.choose k).factorization p ≤ 1

Tactic:
apply factorization_choose_le_log.trans

Result:
p n k : ℕ
p_large : n < p ^ 2
⊢ log p n ≤ 1

Proof state:
case inr
p n k : ℕ
p_large : n < p ^ 2
hn0 : n ≠ 0
⊢ log p n ≤ 1

Tactic:
exact Nat.lt_succ_iff.1 (log_lt_of_lt_pow hn0 p_large)

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Card.lean
theorem generateMeasurableRec_of_omega1_le (s : Set (Set α)) {i : Ordinal.{v}} (hi : ω₁ ≤ i) :
    generateMeasurableRec s i = generateMeasurableRec s (ω₁ : Ordinal.{v})

Proof state:
α : Type u
s : Set (Set α)
i : Ordinal.{v}
hi : ω_ 1 ≤ i
⊢ generateMeasurableRec s i ≤ {t | GenerateMeasurable s t}

Tactic:
exact generateMeasurableRec_subset s i

Result:
no goals

Proof state:
α : Type u
s : Set (Set α)
i : Ordinal.{v}
hi : ω_ 1 ≤ i
⊢ generateMeasurableRec s i ≤ generateMeasurableRec s (ω_ 1)

Tactic:
rw [← generateMeasurable_eq_rec]

Result:
α : Type u
s : Set (Set α)
i : Ordinal.{v}
hi : ω_ 1 ≤ i
⊢ generateMeasurableRec s i ≤ {t | GenerateMeasurable s t}

Proof state:
α : Type u
s : Set (Set α)
i : Ordinal.{v}
hi : ω_ 1 ≤ i
⊢ generateMeasurableRec s i = generateMeasurableRec s (ω_ 1)

Tactic:
apply (generateMeasurableRec_mono s hi).antisymm'

Result:
α : Type u
s : Set (Set α)
i : Ordinal.{v}
hi : ω_ 1 ≤ i
⊢ generateMeasurableRec s i ≤ generateMeasurableRec s (ω_ 1)
-- Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
theorem unique_irreducible (hR : HasUnitMulPowIrreducibleFactorization R)
    ⦃p q : R⦄ (hp : Irreducible p) (hq : Irreducible q) :
    Associated p q

Proof state:
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
⊢ ∀ n < 1, n = 0

Tactic:
decide

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝ : CommRing R
p q : R
hp : Irreducible p
hq : Irreducible q
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
⊢ ∀ {p : R}, Irreducible p → Associated p ϖ

Tactic:
clear hp hq p q

Result:
case intro.intro
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
⊢ ∀ {p : R}, Irreducible p → Associated p ϖ

Proof state:
case intro.intro.intro.inl
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ n) p
this : Irreducible (ϖ ^ n)
H : n < 1
⊢ Associated p ϖ

Tactic:
obtain rfl : n = 0 := by
  clear hn this
  revert H n
  decide

Result:
case intro.intro.intro.inl
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
hn : Associated (ϖ ^ 0) p
this : Irreducible (ϖ ^ 0)
H : 0 < 1
⊢ Associated p ϖ

Proof state:
case intro.intro.intro.inr.inr.intro.inr
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ (1 + n + 1)) p
this : Irreducible (ϖ * ϖ ^ (1 + n))
H : 1 < 1 + n + 1
H0 : IsUnit (ϖ ^ (1 + n))
⊢ Associated p ϖ

Tactic:
rw [add_comm, pow_succ'] at H0

Result:
case intro.intro.intro.inr.inr.intro.inr
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ (1 + n + 1)) p
this : Irreducible (ϖ * ϖ ^ (1 + n))
H : 1 < 1 + n + 1
H0 : IsUnit (ϖ * ϖ ^ n)
⊢ Associated p ϖ

Proof state:
R : Type u_1
inst✝ : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
p q : R
hp : Irreducible p
hq : Irreducible q
⊢ Associated p q

Tactic:
rcases hR with ⟨ϖ, hϖ, hR⟩

Result:
case intro.intro
R : Type u_1
inst✝ : CommRing R
p q : R
hp : Irreducible p
hq : Irreducible q
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
⊢ Associated p q
-- Mathlib/Data/Real/Archimedean.lean
theorem iUnion_Iic_rat : ⋃ r : ℚ, Iic (r : ℝ) = univ

Proof state:
⊢ ⋃ r, Iic ↑r = univ

Tactic:
exact iUnion_Iic_of_not_bddAbove_range not_bddAbove_coe

Result:
no goals
-- Mathlib/CategoryTheory/PathCategory/Basic.lean
theorem composePath_comp {X Y Z : C} (f : Path X Y) (g : Path Y Z) :
    composePath (f.comp g) = composePath f ≫ composePath g

Proof state:
case nil
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Path X Y
⊢ composePath (f.comp Path.nil) = composePath f ≫ composePath Path.nil

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Path X Y
g : Path Y Z
⊢ composePath (f.comp g) = composePath f ≫ composePath g

Tactic:
induction' g with Y' Z' g e ih

Result:
case nil
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Path X Y
⊢ composePath (f.comp Path.nil) = composePath f ≫ composePath Path.nil

case cons
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Path X Y
Y' Z' : C
g : Path Y Y'
e : Y' ⟶ Z'
ih : composePath (f.comp g) = composePath f ≫ composePath g
⊢ composePath (f.comp (g.cons e)) = composePath f ≫ composePath (g.cons e)

Proof state:
case cons
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Path X Y
Y' Z' : C
g : Path Y Y'
e : Y' ⟶ Z'
ih : composePath (f.comp g) = composePath f ≫ composePath g
⊢ composePath (f.comp (g.cons e)) = composePath f ≫ composePath (g.cons e)

Tactic:
simp [ih]

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem GoodProducts.spanFin [WellFoundedLT I] :
    ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C (· ∈ s))))

Proof state:
case neg.h₁.hx
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x => x ∈ s)
l : List I := Finset.sort (fun x1 x2 => x1 ≥ x2) s
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    e (π C fun x => x ∈ s) a * c.sum g = c.sum fun a_1 b => e (π C fun x => x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
⊢ (c.sum fun a_1 b => e (π C fun x => x ∈ s) a * b • Products.eval (π C fun x => x ∈ s) a_1) ∈
    Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
exact finsupp_sum_mem_span_eval _ _ ha hc

Result:
no goals

Proof state:
case intro.cons
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x => x ∈ s)
l : List I := Finset.sort (fun x1 x2 => x1 ≥ x2) s
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
ih :
  ∃ l,
    ↑l.support ⊆ {m | ↑m ≤ as} ∧
      (l.sum fun i a => a • Products.eval (π C fun x => x ∈ s) i) =
        (List.map (fun i => if ↑x i = true then e (π C fun x => x ∈ s) i else 1 - e (π C fun x => x ∈ s) i) as).prod
⊢ (if ↑x a = true then e (π C fun x => x ∈ s) a else 1 - e (π C fun x => x ∈ s) a) *
      (List.map (fun i => if ↑x i = true then e (π C fun x => x ∈ s) i else 1 - e (π C fun x => x ∈ s) i) as).prod ∈
    Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
obtain ⟨c, hc, hc'⟩ := ih

Result:
case intro.cons.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x => x ∈ s)
l : List I := Finset.sort (fun x1 x2 => x1 ≥ x2) s
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
hc' :
  (c.sum fun i a => a • Products.eval (π C fun x => x ∈ s) i) =
    (List.map (fun i => if ↑x i = true then e (π C fun x => x ∈ s) i else 1 - e (π C fun x => x ∈ s) i) as).prod
⊢ (if ↑x a = true then e (π C fun x => x ∈ s) a else 1 - e (π C fun x => x ∈ s) a) *
      (List.map (fun i => if ↑x i = true then e (π C fun x => x ∈ s) i else 1 - e (π C fun x => x ∈ s) i) as).prod ∈
    Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x => x ∈ s)
l : List I := Finset.sort (fun x1 x2 => x1 ≥ x2) s
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    e (π C fun x => x ∈ s) a * c.sum g = c.sum fun a_1 b => e (π C fun x => x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
m : Products I
hm : c m ≠ 0
⊢ m ∈ ↑c.support

Tactic:
simpa only [Finset.mem_coe, Finsupp.mem_support_iff] using hm

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
private lemma trans_aux (hst : toColex s ≤ toColex t) (htu : toColex t ≤ toColex u)
    (has : a ∈ s) (hat : a ∉ t) : ∃ b, b ∈ u ∧ b ∉ s ∧ a ≤ b

Proof state:
case neg
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
htu : { ofColex := t } ≤ { ofColex := u }
has : a ∈ s
hat : a ∉ t
s' : Finset α := filter (fun b => b ∉ t ∧ a ≤ b) s
b : α
hb : b ∈ s ∧ b ∉ t ∧ a ≤ b
hbmax : ∀ x ∈ s, x ∉ t → a ≤ x → ¬b < x
c : α
hct : c ∈ { ofColex := t }.ofColex
hcs : c ∉ { ofColex := s }.ofColex
hbc : b ≤ c
hcu : c ∉ u
d : α
hdu : d ∈ { ofColex := u }.ofColex
hdt : d ∉ { ofColex := t }.ofColex
hcd : c ≤ d
had : a ≤ d
hds : d ∈ s
⊢ False

Tactic:
exact hbmax d hds hdt had <| hbc.trans_lt <| hcd.lt_of_ne <| ne_of_mem_of_not_mem hct hdt

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
htu : { ofColex := t } ≤ { ofColex := u }
has : a ∈ s
hat : a ∉ t
s' : Finset α := filter (fun b => b ∉ t ∧ a ≤ b) s
⊢ a ∈ s'

Tactic:
simp [s', has, hat]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/End.lean
theorem _root_.Module.End_isUnit_inv_apply_apply_of_isUnit
    {f : Module.End R M} (h : IsUnit f) (x : M) :
    h.unit.inv (f x) = x :=
  (by simp : (h.unit.inv * f) x = x)

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : Module.End R M
h : IsUnit f
x : M
⊢ (h.unit.inv * f) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem lt_of_getMsbD {x : BitVec w} {i : Nat} : getMsbD x i = true → i < w

Proof state:
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ x.getMsbD i = true → i < w

Tactic:
simp [h]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Nat
⊢ x.getMsbD i = true → i < w

Tactic:
if h : i < w then
  simp [h]
else
  simp [Nat.ge_of_not_lt h]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Nat
h : ¬i < w
⊢ x.getMsbD i = true → i < w

Tactic:
simp [Nat.ge_of_not_lt h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem mergeSort_nil : [].mergeSort r = []

Proof state:
α✝ : Type u_1
r : α✝ → α✝ → Bool
⊢ [].mergeSort r = []

Tactic:
rw [List.mergeSort]

Result:
no goals
-- Mathlib/Algebra/Module/Card.lean
theorem mk_le_of_module (R : Type u) (E : Type v)
    [AddCommGroup E] [Ring R] [Module R E] [Nontrivial E] [NoZeroSMulDivisors R E] :
    Cardinal.lift.{v} (#R) ≤ Cardinal.lift.{u} (#E)

Proof state:
case intro
R : Type u
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Ring R
inst✝² : Module R E
inst✝¹ : Nontrivial E
inst✝ : NoZeroSMulDivisors R E
x : E
hx : x ≠ 0
⊢ lift.{v, u} #R ≤ lift.{u, v} #E

Tactic:
have : Injective (fun k ↦ k • x) := smul_left_injective R hx

Result:
case intro
R : Type u
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Ring R
inst✝² : Module R E
inst✝¹ : Nontrivial E
inst✝ : NoZeroSMulDivisors R E
x : E
hx : x ≠ 0
this : Injective fun k => k • x
⊢ lift.{v, u} #R ≤ lift.{u, v} #E

Proof state:
R : Type u
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Ring R
inst✝² : Module R E
inst✝¹ : Nontrivial E
inst✝ : NoZeroSMulDivisors R E
⊢ lift.{v, u} #R ≤ lift.{u, v} #E

Tactic:
obtain ⟨x, hx⟩ : ∃ (x : E), x ≠ 0 := exists_ne 0

Result:
case intro
R : Type u
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Ring R
inst✝² : Module R E
inst✝¹ : Nontrivial E
inst✝ : NoZeroSMulDivisors R E
x : E
hx : x ≠ 0
⊢ lift.{v, u} #R ≤ lift.{u, v} #E

Proof state:
case intro
R : Type u
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Ring R
inst✝² : Module R E
inst✝¹ : Nontrivial E
inst✝ : NoZeroSMulDivisors R E
x : E
hx : x ≠ 0
this : Injective fun k => k • x
⊢ lift.{v, u} #R ≤ lift.{u, v} #E

Tactic:
exact lift_mk_le_lift_mk_of_injective this

Result:
no goals