harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem principal_add_iff_add_left_eq_self : Principal (· + ·) o ↔ ∀ a < o, a + o = o

Proof state:
o : Ordinal.{u}
⊢ Principal (fun x1 x2 => x1 + x2) o ↔ ∀ a < o, a + o = o

Tactic:
refine ⟨fun ho a hao => ?_, fun h a b hao hbo => ?_⟩

Result:
case refine_1
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 + x2) o
a : Ordinal.{u}
hao : a < o
⊢ a + o = o

case refine_2
o : Ordinal.{u}
h : ∀ a < o, a + o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun x1 x2 => x1 + x2) a b < o

Proof state:
case refine_1.inr.inr
a : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 + x2) 1
hao : a = 0
ho₁ : 1 ≤ 1
⊢ a + 1 = 1

Tactic:
rw [hao, zero_add]

Result:
no goals

Proof state:
case refine_1.inl
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 + x2) o
a : Ordinal.{u}
hao : a < o
ho₁ : 1 < o
⊢ a + o = o

Tactic:
exact op_eq_self_of_principal hao (isNormal_add_right a) ho (isLimit_of_principal_add ho₁ ho)

Result:
no goals

Proof state:
case refine_2
o : Ordinal.{u}
h : ∀ a < o, a + o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun x1 x2 => x1 + x2) a b < o

Tactic:
rw [← h a hao]

Result:
case refine_2
o : Ordinal.{u}
h : ∀ a < o, a + o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun x1 x2 => x1 + x2) a b < a + o

Proof state:
case refine_2
o : Ordinal.{u}
h : ∀ a < o, a + o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun x1 x2 => x1 + x2) a b < a + o

Tactic:
exact (isNormal_add_right a).strictMono hbo

Result:
no goals

Proof state:
case refine_1.inr.inr
a : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 + x2) 1
hao : a < 1
ho₁ : 1 ≤ 1
⊢ a + 1 = 1

Tactic:
rw [lt_one_iff_zero] at hao

Result:
case refine_1.inr.inr
a : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 + x2) 1
hao : a = 0
ho₁ : 1 ≤ 1
⊢ a + 1 = 1

Proof state:
case refine_1.inr.inl
a : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 + x2) 0
hao : a < 0
ho₁ : 0 ≤ 1
⊢ a + 0 = 0

Tactic:
exact (Ordinal.not_lt_zero a hao).elim

Result:
no goals

Proof state:
case refine_1
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 + x2) o
a : Ordinal.{u}
hao : a < o
⊢ a + o = o

Tactic:
rcases lt_or_le 1 o with ho₁ | ho₁

Result:
case refine_1.inl
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 + x2) o
a : Ordinal.{u}
hao : a < o
ho₁ : 1 < o
⊢ a + o = o

case refine_1.inr
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 + x2) o
a : Ordinal.{u}
hao : a < o
ho₁ : o ≤ 1
⊢ a + o = o

Proof state:
case refine_1.inr
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 + x2) o
a : Ordinal.{u}
hao : a < o
ho₁ : o ≤ 1
⊢ a + o = o

Tactic:
rcases le_one_iff.1 ho₁ with (rfl | rfl)

Result:
case refine_1.inr.inl
a : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 + x2) 0
hao : a < 0
ho₁ : 0 ≤ 1
⊢ a + 0 = 0

case refine_1.inr.inr
a : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 + x2) 1
hao : a < 1
ho₁ : 1 ≤ 1
⊢ a + 1 = 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem IsPrefix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) :
    l₁.filter p <+: l₂.filter p

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : l₁ <+: l₂
⊢ List.filter p l₁ <+: List.filter p l₂

Tactic:
obtain ⟨xs, rfl⟩ := h

Result:
case intro
α : Type u_1
p : α → Bool
l₁ xs : List α
⊢ List.filter p l₁ <+: List.filter p (l₁ ++ xs)

Proof state:
case intro
α : Type u_1
p : α → Bool
l₁ xs : List α
⊢ List.filter p l₁ <+: List.filter p l₁ ++ List.filter p xs

Tactic:
apply prefix_append

Result:
no goals

Proof state:
case intro
α : Type u_1
p : α → Bool
l₁ xs : List α
⊢ List.filter p l₁ <+: List.filter p (l₁ ++ xs)

Tactic:
rw [filter_append]

Result:
case intro
α : Type u_1
p : α → Bool
l₁ xs : List α
⊢ List.filter p l₁ <+: List.filter p l₁ ++ List.filter p xs
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_biUnion {I : Set ι} {t : ι → Set α} (h : I.PairwiseDisjoint t) (hI : I.Finite)
    (ht : ∀ i ∈ I, (t i).Finite) : ∏ᶠ a ∈ ⋃ x ∈ I, t x, f a = ∏ᶠ i ∈ I, ∏ᶠ j ∈ t i, f j

Proof state:
case h
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝ : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype ↑I
⊢ Pairwise (Disjoint on fun x => t ↑x)

case ht
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝ : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype ↑I
⊢ ∀ (i : ↑I), (t ↑i).Finite

Tactic:
exacts [fun x y hxy => h x.2 y.2 (Subtype.coe_injective.ne hxy), fun b => ht b b.2]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝ : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ x ∈ I, t x), f a = ∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j

Tactic:
haveI := hI.fintype

Result:
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝ : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype ↑I
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ x ∈ I, t x), f a = ∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j

Proof state:
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝ : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype ↑I
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ x ∈ I, t x), f a = ∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j

Tactic:
rw [biUnion_eq_iUnion, finprod_mem_iUnion, ← finprod_set_coe_eq_finprod_mem]

Result:
case h
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝ : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype ↑I
⊢ Pairwise (Disjoint on fun x => t ↑x)

case ht
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝ : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype ↑I
⊢ ∀ (i : ↑I), (t ↑i).Finite
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive (attr := simp)]
lemma pow_iterate (k : ℕ) : ∀ n : ℕ, (fun x : M ↦ x ^ k)^[n] = (· ^ k ^ n)
  | 0 => by ext; simp
  | n + 1 => by ext; simp [pow_iterate, Nat.pow_succ', pow_mul]

Proof state:
M : Type u_4
inst✝ : Monoid M
k n : ℕ
⊢ (fun x => x ^ k)^[n + 1] = fun x => x ^ k ^ (n + 1)

Tactic:
ext

Result:
case h
M : Type u_4
inst✝ : Monoid M
k n : ℕ
x✝ : M
⊢ (fun x => x ^ k)^[n + 1] x✝ = x✝ ^ k ^ (n + 1)

Proof state:
case h
M : Type u_4
inst✝ : Monoid M
k : ℕ
x✝ : M
⊢ (fun x => x ^ k)^[0] x✝ = x✝ ^ k ^ 0

Tactic:
simp

Result:
no goals

Proof state:
case h
M : Type u_4
inst✝ : Monoid M
k n : ℕ
x✝ : M
⊢ (fun x => x ^ k)^[n + 1] x✝ = x✝ ^ k ^ (n + 1)

Tactic:
simp [pow_iterate, Nat.pow_succ', pow_mul]

Result:
no goals

Proof state:
M : Type u_4
inst✝ : Monoid M
k : ℕ
⊢ (fun x => x ^ k)^[0] = fun x => x ^ k ^ 0

Tactic:
ext

Result:
case h
M : Type u_4
inst✝ : Monoid M
k : ℕ
x✝ : M
⊢ (fun x => x ^ k)^[0] x✝ = x✝ ^ k ^ 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_append_of_containsKey_eq_false [BEq α] {l l' : List ((a : α) × β a)} {a : α}
    (h : containsKey a l' = false) : getEntry? a (l ++ l') = getEntry? a l

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l l' : List ((a : α) × β a)
a : α
h : containsKey a l' = false
⊢ getEntry? a (l ++ l') = getEntry? a l

Tactic:
rw [getEntry?_append, getEntry?_eq_none.2 h, Option.or_none]

Result:
no goals
-- Mathlib/ModelTheory/DirectLimit.lean
theorem unify_sigma_mk_self {α : Type*} {i : ι} {x : α → G i} :
    (unify f (fun a => .mk f i (x a)) i fun _ ⟨_, hj⟩ =>
      _root_.trans (le_of_eq hj.symm) (refl _)) = x

Proof state:
case h
L : Language
ι : Type v
inst✝² : Preorder ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
α : Type u_1
i : ι
x : α → G i
a : α
⊢ unify f (fun a => Structure.Sigma.mk f i (x a)) i ⋯ a = x a

Tactic:
rw [unify]

Result:
case h
L : Language
ι : Type v
inst✝² : Preorder ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
α : Type u_1
i : ι
x : α → G i
a : α
⊢ (f (Structure.Sigma.mk f i (x a)).fst i ⋯) (Structure.Sigma.mk f i (x a)).snd = x a

Proof state:
case h
L : Language
ι : Type v
inst✝² : Preorder ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
α : Type u_1
i : ι
x : α → G i
a : α
⊢ (f (Structure.Sigma.mk f i (x a)).fst i ⋯) (Structure.Sigma.mk f i (x a)).snd = x a

Tactic:
apply DirectedSystem.map_self

Result:
no goals

Proof state:
L : Language
ι : Type v
inst✝² : Preorder ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
α : Type u_1
i : ι
x : α → G i
⊢ unify f (fun a => Structure.Sigma.mk f i (x a)) i ⋯ = x

Tactic:
ext a

Result:
case h
L : Language
ι : Type v
inst✝² : Preorder ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
α : Type u_1
i : ι
x : α → G i
a : α
⊢ unify f (fun a => Structure.Sigma.mk f i (x a)) i ⋯ a = x a
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioc_union_Ioc_left : Ioc a c ∪ Ioc b c = Ioc (min a b) c

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ Ioc a c ∪ Ioc b c = Ioc (a ⊓ b) c

Tactic:
rw [Ioc_union_Ioc, max_self] <;> exact (min_le_right _ _).trans (le_max_right _ _)

Result:
no goals
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem RingHom.isSemisimpleRing_of_surjective (f : R →+* S) (hf : Function.Surjective f)
    [IsSemisimpleRing R] : IsSemisimpleRing S

Proof state:
R : Type u_2
S : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsSemisimpleRing R
this : Module R S := Module.compHom S f
⊢ IsSemisimpleRing S

Tactic:
haveI : RingHomSurjective f := ⟨hf⟩

Result:
R : Type u_2
S : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsSemisimpleRing R
this✝ : Module R S := Module.compHom S f
this : RingHomSurjective f
⊢ IsSemisimpleRing S

Proof state:
R : Type u_2
S : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsSemisimpleRing R
this✝ : Module R S := Module.compHom S f
this : RingHomSurjective f
e : S →ₛₗ[f] S :=
  let __src := AddMonoidHom.id S;
  { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ IsSemisimpleModule R S

Tactic:
infer_instance

Result:
no goals

Proof state:
R : Type u_2
S : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsSemisimpleRing R
this✝ : Module R S := Module.compHom S f
this : RingHomSurjective f
⊢ IsSemisimpleRing S

Tactic:
let e : S →ₛₗ[f] S := { AddMonoidHom.id S with map_smul' := fun _ _ ↦ rfl }

Result:
R : Type u_2
S : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsSemisimpleRing R
this✝ : Module R S := Module.compHom S f
this : RingHomSurjective f
e : S →ₛₗ[f] S :=
  let __src := AddMonoidHom.id S;
  { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ IsSemisimpleRing S

Proof state:
R : Type u_2
S : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsSemisimpleRing R
this✝ : Module R S := Module.compHom S f
this : RingHomSurjective f
e : S →ₛₗ[f] S :=
  let __src := AddMonoidHom.id S;
  { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ IsSemisimpleRing S

Tactic:
rw [IsSemisimpleRing, ← e.isSemisimpleModule_iff_of_bijective Function.bijective_id]

Result:
R : Type u_2
S : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsSemisimpleRing R
this✝ : Module R S := Module.compHom S f
this : RingHomSurjective f
e : S →ₛₗ[f] S :=
  let __src := AddMonoidHom.id S;
  { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ IsSemisimpleModule R S

Proof state:
R : Type u_2
S : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsSemisimpleRing R
⊢ IsSemisimpleRing S

Tactic:
letI : Module R S := Module.compHom _ f

Result:
R : Type u_2
S : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsSemisimpleRing R
this : Module R S := Module.compHom S f
⊢ IsSemisimpleRing S
-- Mathlib/Algebra/Group/Subgroup/Map.lean
theorem subgroupOf_eq_bot {H K : Subgroup G} : H.subgroupOf K = ⊥ ↔ Disjoint H K

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.subgroupOf K = ⊥ ↔ Disjoint H K

Tactic:
rw [disjoint_iff, ← bot_subgroupOf, subgroupOf_inj, bot_inf_eq]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem setOf_pow_dvd_eq_Icc_factorization {n p : ℕ} (pp : p.Prime) (hn : n ≠ 0) :
    { i : ℕ | i ≠ 0 ∧ p ^ i ∣ n } = Set.Icc 1 (n.factorization p)

Proof state:
case h
n p : ℕ
pp : Prime p
hn : n ≠ 0
x✝ : ℕ
⊢ x✝ ∈ {i | i ≠ 0 ∧ p ^ i ∣ n} ↔ x✝ ∈ Set.Icc 1 (n.factorization p)

Tactic:
simp [Nat.lt_succ_iff, one_le_iff_ne_zero, pp.pow_dvd_iff_le_factorization hn]

Result:
no goals

Proof state:
n p : ℕ
pp : Prime p
hn : n ≠ 0
⊢ {i | i ≠ 0 ∧ p ^ i ∣ n} = Set.Icc 1 (n.factorization p)

Tactic:
ext

Result:
case h
n p : ℕ
pp : Prime p
hn : n ≠ 0
x✝ : ℕ
⊢ x✝ ∈ {i | i ≠ 0 ∧ p ^ i ∣ n} ↔ x✝ ∈ Set.Icc 1 (n.factorization p)
-- Mathlib/Analysis/InnerProductSpace/Orientation.lean
theorem volumeForm_zero_pos [_i : Fact (finrank ℝ E = 0)] :
    Orientation.volumeForm (positiveOrientation : Orientation ℝ E (Fin 0)) =
      AlternatingMap.constLinearEquivOfIsEmpty 1

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ positiveOrientation.volumeForm = AlternatingMap.constLinearEquivOfIsEmpty 1

Tactic:
simp [volumeForm, Or.by_cases, if_pos]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem letFun_val_congr {α : Sort u} {β : Sort v} {a a' : α} {f : α → β} (h : a = a')
    : @letFun α (fun _ => β) a f = @letFun α (fun _ => β) a' f

Proof state:
α : Sort u
β : Sort v
a a' : α
f : α → β
h : a = a'
⊢ letFun a f = letFun a' f

Tactic:
rw [h]

Result:
no goals
-- Mathlib/ModelTheory/Substructures.lean
theorem reduct_withConstants :
    (L.lhomWithConstants A).substructureReduct (S.withConstants h) = S

Proof state:
case h
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
A : Set M
h : A ⊆ ↑S
x✝ : M
⊢ x✝ ∈ (L.lhomWithConstants ↑A).substructureReduct (S.withConstants h) ↔ x✝ ∈ S

Tactic:
simp

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
A : Set M
h : A ⊆ ↑S
⊢ (L.lhomWithConstants ↑A).substructureReduct (S.withConstants h) = S

Tactic:
ext

Result:
case h
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
A : Set M
h : A ⊆ ↑S
x✝ : M
⊢ x✝ ∈ (L.lhomWithConstants ↑A).substructureReduct (S.withConstants h) ↔ x✝ ∈ S
-- Mathlib/Data/Finset/Image.lean
theorem image_erase [DecidableEq α] {f : α → β} (hf : Injective f) (s : Finset α) (a : α) :
    (s.erase a).image f = (s.image f).erase (f a) :=
  coe_injective <| by push_cast [Set.image_diff hf, Set.image_singleton]; rfl

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α → β
hf : Injective f
s : Finset α
a : α
⊢ ↑(image f (s.erase a)) = ↑((image f s).erase (f a))

Tactic:
push_cast [Set.image_diff hf, Set.image_singleton]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α → β
hf : Injective f
s : Finset α
a : α
⊢ f '' ↑s \ {f a} = f '' ↑s \ {f a}

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α → β
hf : Injective f
s : Finset α
a : α
⊢ f '' ↑s \ {f a} = f '' ↑s \ {f a}

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem erase_sdiff_distrib (s t : Finset α) (a : α) : (s \ t).erase a = s.erase a \ t.erase a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ (s \ t).erase a = s.erase a \ t.erase a

Tactic:
simp_rw [erase_eq, sdiff_sdiff, sup_sdiff_eq_sup le_rfl, sup_comm]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
theorem mapShortComplexH2_id :
    mapShortComplexH2 (MonoidHom.id _) (𝟙 A) = 𝟙 _

Proof state:
k H : Type u
inst✝¹ : CommRing k
inst✝ : Group H
A : Rep k H
⊢ mapShortComplexH2 (MonoidHom.id H) (𝟙 A) = 𝟙 (shortComplexH2 A)

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
lemma isZero₃_iff : IsZero T.obj₃ ↔ (T.mor₂ = 0 ∧ T.mor₃ = 0)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ IsZero T.obj₃ ↔ T.mor₂ = 0 ∧ T.mor₃ = 0

Tactic:
refine (isZero₂_iff _ (rot_of_distTriang _ hT)).trans ?_

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ T.rotate.mor₁ = 0 ∧ T.rotate.mor₂ = 0 ↔ T.mor₂ = 0 ∧ T.mor₃ = 0

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ T.mor₂ = 0 ∧ T.mor₃ = 0 ↔ T.mor₂ = 0 ∧ T.mor₃ = 0

Tactic:
tauto

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ T.rotate.mor₁ = 0 ∧ T.rotate.mor₂ = 0 ↔ T.mor₂ = 0 ∧ T.mor₃ = 0

Tactic:
dsimp

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ T.mor₂ = 0 ∧ T.mor₃ = 0 ↔ T.mor₂ = 0 ∧ T.mor₃ = 0
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
@[simp]
lemma coeff_Φ (n : ℤ) : (W.Φ n).coeff (n.natAbs ^ 2) = 1

Proof state:
case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.Φ ↑n).coeff ((↑n).natAbs ^ 2) = 1
n✝ : ℕ
⊢ (W.Φ (-↑n✝)).coeff ((-↑n✝).natAbs ^ 2) = 1

Tactic:
simp only [Φ_neg, Int.natAbs_neg, ih]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (W.Φ n).coeff (n.natAbs ^ 2) = 1

Tactic:
induction n using Int.negInduction with
| nat n => exact (W.natDegree_coeff_Φ_ofNat n).right
| neg ih => simp only [Φ_neg, Int.natAbs_neg, ih]

Result:
no goals

Proof state:
case nat
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (W.Φ ↑n).coeff ((↑n).natAbs ^ 2) = 1

Tactic:
exact (W.natDegree_coeff_Φ_ofNat n).right

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem uniformContinuous_toFun (h : ⋃₀ 𝔖 = univ) :
    UniformContinuous (toFun 𝔖 : (α →ᵤ[𝔖] β) → α → β)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
⊢ ∀ (i : α), UniformContinuous fun x => (toFun 𝔖) x i

Tactic:
exact uniformContinuous_eval h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
⊢ UniformContinuous ⇑(toFun 𝔖)

Tactic:
rw [uniformContinuous_pi]

Result:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
⊢ ∀ (i : α), UniformContinuous fun x => (toFun 𝔖) x i
-- Mathlib/Computability/NFA.lean
theorem toDFA_correct : M.toDFA.accepts = M.accepts

Proof state:
case h
α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ x ∈ M.toDFA.accepts ↔ x ∈ M.accepts

Tactic:
rw [mem_accepts, DFA.mem_accepts]

Result:
case h
α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ M.toDFA.eval x ∈ M.toDFA.accept ↔ ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x

Proof state:
case h.mpr
α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ (∃ S ∈ M.accept, S ∈ M.evalFrom M.start x) → M.toDFA.eval x ∈ M.toDFA.accept

Tactic:
exact fun ⟨w, h2, h3⟩ => ⟨w, h3, h2⟩

Result:
no goals

Proof state:
α : Type u
σ : Type v
M : NFA α σ
⊢ M.toDFA.accepts = M.accepts

Tactic:
ext x

Result:
case h
α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ x ∈ M.toDFA.accepts ↔ x ∈ M.accepts
-- Mathlib/Algebra/Homology/HomologicalComplexBiprod.lean
@[reassoc (attr := simp)]
lemma biprod_inl_desc_f (α : K ⟶ M) (β : L ⟶ M) (i : ι) :
    (biprod.inl : K ⟶ K ⊞ L).f i ≫ (biprod.desc α β).f i = α.f i

Proof state:
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
M : HomologicalComplex C c
α : K ⟶ M
β : L ⟶ M
i : ι
⊢ biprod.inl.f i ≫ (biprod.desc α β).f i = α.f i

Tactic:
rw [← comp_f, biprod.inl_desc]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem smul (H : InnerRegularWRT μ p q) (c : ℝ≥0∞) : InnerRegularWRT (c • μ) p q

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
H : μ.InnerRegularWRT p q
c : ℝ≥0∞
U : Set α
hU : q U
r : ℝ≥0∞
hr : r < (c • μ) U
⊢ ∃ K ⊆ U, p K ∧ r < (c • μ) K

Tactic:
rw [smul_apply, H.measure_eq_iSup hU, smul_eq_mul] at hr

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
H : μ.InnerRegularWRT p q
c : ℝ≥0∞
U : Set α
hU : q U
r : ℝ≥0∞
hr : r < c * ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : p K), μ K
⊢ ∃ K ⊆ U, p K ∧ r < (c • μ) K

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
H : μ.InnerRegularWRT p q
c : ℝ≥0∞
U : Set α
hU : q U
r : ℝ≥0∞
hr : r < c * ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : p K), μ K
⊢ ∃ K ⊆ U, p K ∧ r < (c • μ) K

Tactic:
simpa only [ENNReal.mul_iSup, lt_iSup_iff, exists_prop] using hr

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
H : μ.InnerRegularWRT p q
c : ℝ≥0∞
⊢ (c • μ).InnerRegularWRT p q

Tactic:
intro U hU r hr

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
H : μ.InnerRegularWRT p q
c : ℝ≥0∞
U : Set α
hU : q U
r : ℝ≥0∞
hr : r < (c • μ) U
⊢ ∃ K ⊆ U, p K ∧ r < (c • μ) K
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_natCast (x : ℝ≥0∞) (n : ℕ) : x ^ (n : ℝ) = x ^ n

Proof state:
case coe
n : ℕ
x✝ : ℝ≥0
⊢ ↑x✝ ^ ↑n = ↑x✝ ^ n

Tactic:
simp [← coe_rpow_of_nonneg _ (Nat.cast_nonneg n)]

Result:
no goals

Proof state:
case top
n : ℕ
⊢ ⊤ ^ ↑n = ⊤ ^ n

Tactic:
cases n <;> simp [top_rpow_of_pos (Nat.cast_add_one_pos _), top_pow (Nat.succ_pos _)]

Result:
no goals

Proof state:
x : ℝ≥0∞
n : ℕ
⊢ x ^ ↑n = x ^ n

Tactic:
cases x

Result:
case top
n : ℕ
⊢ ⊤ ^ ↑n = ⊤ ^ n

case coe
n : ℕ
x✝ : ℝ≥0
⊢ ↑x✝ ^ ↑n = ↑x✝ ^ n
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Ico_succ_right_eq_Icc (a b : α) : Ico a (succ b) = Icc a b := coe_injective <| by simp

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ ↑(Ico a (succ b)) = ↑(Icc a b)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem isSimpleModule_iff_isCoatom : IsSimpleModule R (M ⧸ m) ↔ IsCoatom m

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : Submodule R M
⊢ IsSimpleModule R (M ⧸ m) ↔ IsSimpleOrder ↑(Set.Ici m)

Tactic:
apply OrderIso.isSimpleOrder_iff

Result:
case f
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : Submodule R M
⊢ Submodule R (M ⧸ m) ≃o ↑(Set.Ici m)

Proof state:
case f
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : Submodule R M
⊢ Submodule R (M ⧸ m) ≃o ↑(Set.Ici m)

Tactic:
exact Submodule.comapMkQRelIso m

Result:
no goals

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : Submodule R M
⊢ IsSimpleModule R (M ⧸ m) ↔ IsCoatom m

Tactic:
rw [← Set.isSimpleOrder_Ici_iff_isCoatom]

Result:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : Submodule R M
⊢ IsSimpleModule R (M ⧸ m) ↔ IsSimpleOrder ↑(Set.Ici m)