harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem hsum_add {s t : SummableFamily Γ R α} : (s + t).hsum = s.hsum + t.hsum

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s t : SummableFamily Γ R α
g : Γ
⊢ ∑ᶠ (i : α), ((s i).coeff g + (t i).coeff g) = ∑ᶠ (i : α), (s i).coeff g + ∑ᶠ (i : α), (t i).coeff g

Tactic:
exact finsum_add_distrib (s.finite_co_support _) (t.finite_co_support _)

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s t : SummableFamily Γ R α
⊢ (s + t).hsum = s.hsum + t.hsum

Tactic:
ext g

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s t : SummableFamily Γ R α
g : Γ
⊢ (s + t).hsum.coeff g = (s.hsum + t.hsum).coeff g

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s t : SummableFamily Γ R α
g : Γ
⊢ (s + t).hsum.coeff g = (s.hsum + t.hsum).coeff g

Tactic:
simp only [coeff_hsum, coeff_add, add_apply]

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s t : SummableFamily Γ R α
g : Γ
⊢ ∑ᶠ (i : α), ((s i).coeff g + (t i).coeff g) = ∑ᶠ (i : α), (s i).coeff g + ∑ᶠ (i : α), (t i).coeff g
-- Mathlib/CategoryTheory/Shift/InducedShiftSequence.lean
@[reassoc]
lemma induced_shiftMap {n : M} {X Y : C} (f : X ⟶ Y⟦n⟧) (a a' : M) (h : n + a = a') :
    letI := induced e M F' e'
    F.shiftMap (L.map f ≫ (L.commShiftIso n).hom.app _) a a' h =
      (e' a).hom.app X ≫ G.shiftMap f a a' h ≫ (e' a').inv.app Y

Proof state:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{u_5, u_1} C
inst✝⁸ : Category.{u_7, u_2} D
inst✝⁷ : Category.{u_6, u_3} A
L : C ⥤ D
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n : M
X Y : C
f : X ⟶ (shiftFunctor C n).obj Y
a a' : M
h : n + a = a'
⊢ (F.shift a).map (L.map f ≫ (L.commShiftIso n).hom.app Y) ≫ (F.shiftIso n a a' h).hom.app (L.obj Y) =
    (e' a).hom.app X ≫ ((G.shift a).map f ≫ (G.shiftIso n a a' h).hom.app Y) ≫ (e' a').inv.app Y

Tactic:
rw [Functor.map_comp, induced_shiftIso_hom_app_obj, assoc, assoc]

Result:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{u_5, u_1} C
inst✝⁸ : Category.{u_7, u_2} D
inst✝⁷ : Category.{u_6, u_3} A
L : C ⥤ D
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n : M
X Y : C
f : X ⟶ (shiftFunctor C n).obj Y
a a' : M
h : n + a = a'
⊢ (F.shift a).map (L.map f) ≫
      (F.shift a).map ((L.commShiftIso n).hom.app Y) ≫
        (F.shift a).map ((L.commShiftIso n).inv.app Y) ≫
          (e' a).hom.app ((shiftFunctor C n).obj Y) ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y =
    (e' a).hom.app X ≫ (G.shift a).map f ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y

Proof state:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{u_5, u_1} C
inst✝⁸ : Category.{u_7, u_2} D
inst✝⁷ : Category.{u_6, u_3} A
L : C ⥤ D
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n : M
X Y : C
f : X ⟶ (shiftFunctor C n).obj Y
a a' : M
h : n + a = a'
⊢ (F.shift a).map (L.map f) ≫
      (e' a).hom.app ((shiftFunctor C n).obj Y) ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y =
    (L ⋙ F' a).map f ≫ (e' a).hom.app ((shiftFunctor C n).obj Y) ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Free.lean
theorem mk_freeGroup [Nonempty α] : #(FreeGroup α) = max #α ℵ₀

Proof state:
case a.inl
α : Type u
inst✝ : Nonempty α
hα : #α < ℵ₀
⊢ #α * 2 ≤ ℵ₀

Tactic:
exact (mul_lt_aleph0 hα (nat_lt_aleph0 2)).le

Result:
no goals

Proof state:
α : Type u
inst✝ : Nonempty α
hα : ℵ₀ ≤ #α
⊢ 2 ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
case a
α : Type u
inst✝ : Nonempty α
⊢ #(FreeGroup α) ≤ #α ⊔ ℵ₀

Tactic:
apply (mk_le_of_injective (FreeGroup.toWord_injective (α := α))).trans_eq

Result:
case a
α : Type u
inst✝ : Nonempty α
⊢ #(List (α × Bool)) = #α ⊔ ℵ₀

Proof state:
case a
α : Type u
inst✝ : Nonempty α
⊢ #α ⊔ ℵ₀ ≤ #(FreeGroup α)

Tactic:
apply max_le

Result:
case a.h₁
α : Type u
inst✝ : Nonempty α
⊢ #α ≤ #(FreeGroup α)

case a.h₂
α : Type u
inst✝ : Nonempty α
⊢ ℵ₀ ≤ #(FreeGroup α)

Proof state:
case a.inr
α : Type u
inst✝ : Nonempty α
hα : ℵ₀ ≤ #α
⊢ #α * 2 ⊔ ℵ₀ = #α ⊔ ℵ₀

Tactic:
rw [max_eq_left hα, max_eq_left (hα.trans <| Cardinal.le_mul_right two_ne_zero),
  Cardinal.mul_eq_left hα _ (by simp)]

Result:
α : Type u
inst✝ : Nonempty α
hα : ℵ₀ ≤ #α
⊢ 2 ≤ #α

Proof state:
case a
α : Type u
inst✝ : Nonempty α
⊢ #α * 2 ⊔ ℵ₀ = #α ⊔ ℵ₀

Tactic:
obtain hα | hα := lt_or_le #α ℵ₀

Result:
case a.inl
α : Type u
inst✝ : Nonempty α
hα : #α < ℵ₀
⊢ #α * 2 ⊔ ℵ₀ = #α ⊔ ℵ₀

case a.inr
α : Type u
inst✝ : Nonempty α
hα : ℵ₀ ≤ #α
⊢ #α * 2 ⊔ ℵ₀ = #α ⊔ ℵ₀

Proof state:
α : Type u
inst✝ : Nonempty α
hα : ℵ₀ ≤ #α
⊢ 2 ≤ #α

Tactic:
exact (nat_lt_aleph0 2).le.trans hα

Result:
no goals

Proof state:
case a.h₁
α : Type u
inst✝ : Nonempty α
⊢ #α ≤ #(FreeGroup α)

Tactic:
exact mk_le_of_injective FreeGroup.of_injective

Result:
no goals

Proof state:
case a
α : Type u
inst✝ : Nonempty α
⊢ #(List (α × Bool)) = #α ⊔ ℵ₀

Tactic:
simp [Cardinal.mk_list_eq_max_mk_aleph0]

Result:
case a
α : Type u
inst✝ : Nonempty α
⊢ #α * 2 ⊔ ℵ₀ = #α ⊔ ℵ₀

Proof state:
α : Type u
inst✝ : Nonempty α
⊢ #(FreeGroup α) = #α ⊔ ℵ₀

Tactic:
apply le_antisymm

Result:
case a
α : Type u
inst✝ : Nonempty α
⊢ #(FreeGroup α) ≤ #α ⊔ ℵ₀

case a
α : Type u
inst✝ : Nonempty α
⊢ #α ⊔ ℵ₀ ≤ #(FreeGroup α)

Proof state:
case a.inl
α : Type u
inst✝ : Nonempty α
hα : #α < ℵ₀
⊢ #α * 2 ⊔ ℵ₀ = #α ⊔ ℵ₀

Tactic:
simp only [hα.le, max_eq_right, max_eq_right_iff]

Result:
case a.inl
α : Type u
inst✝ : Nonempty α
hα : #α < ℵ₀
⊢ #α * 2 ≤ ℵ₀

Proof state:
case a.h₂
α : Type u
inst✝ : Nonempty α
⊢ ℵ₀ ≤ #(FreeGroup α)

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Pointwise.lean
theorem MulAction.smul_bijective_of_is_unit
    {M : Type*} [Monoid M] {α : Type*} [MulAction M α] {m : M} (hm : IsUnit m) :
    Function.Bijective (fun (a : α) ↦ m • a)

Proof state:
case h.left
M : Type u_1
inst✝¹ : Monoid M
α : Type u_2
inst✝ : MulAction M α
m : Mˣ
x : α
⊢ (fun a => m⁻¹ • a) ((fun a => ↑m • a) x) = x

Tactic:
simp [← Units.smul_def]

Result:
no goals

Proof state:
case h.right
M : Type u_1
inst✝¹ : Monoid M
α : Type u_2
inst✝ : MulAction M α
m : Mˣ
⊢ Function.RightInverse (fun a => m⁻¹ • a) fun a => ↑m • a

Tactic:
intro x

Result:
case h.right
M : Type u_1
inst✝¹ : Monoid M
α : Type u_2
inst✝ : MulAction M α
m : Mˣ
x : α
⊢ (fun a => ↑m • a) ((fun a => m⁻¹ • a) x) = x

Proof state:
M : Type u_1
inst✝¹ : Monoid M
α : Type u_2
inst✝ : MulAction M α
m : M
hm : IsUnit m
⊢ Function.Bijective fun a => m • a

Tactic:
lift m to Mˣ using hm

Result:
case intro
M : Type u_1
inst✝¹ : Monoid M
α : Type u_2
inst✝ : MulAction M α
m : Mˣ
⊢ Function.Bijective fun a => ↑m • a

Proof state:
case h.right
M : Type u_1
inst✝¹ : Monoid M
α : Type u_2
inst✝ : MulAction M α
m : Mˣ
x : α
⊢ (fun a => ↑m • a) ((fun a => m⁻¹ • a) x) = x

Tactic:
simp [← Units.smul_def]

Result:
no goals

Proof state:
case h
M : Type u_1
inst✝¹ : Monoid M
α : Type u_2
inst✝ : MulAction M α
m : Mˣ
⊢ (Function.LeftInverse (fun a => m⁻¹ • a) fun a => ↑m • a) ∧ Function.RightInverse (fun a => m⁻¹ • a) fun a => ↑m • a

Tactic:
constructor

Result:
case h.left
M : Type u_1
inst✝¹ : Monoid M
α : Type u_2
inst✝ : MulAction M α
m : Mˣ
⊢ Function.LeftInverse (fun a => m⁻¹ • a) fun a => ↑m • a

case h.right
M : Type u_1
inst✝¹ : Monoid M
α : Type u_2
inst✝ : MulAction M α
m : Mˣ
⊢ Function.RightInverse (fun a => m⁻¹ • a) fun a => ↑m • a

Proof state:
case h.left
M : Type u_1
inst✝¹ : Monoid M
α : Type u_2
inst✝ : MulAction M α
m : Mˣ
⊢ Function.LeftInverse (fun a => m⁻¹ • a) fun a => ↑m • a

Tactic:
intro x

Result:
case h.left
M : Type u_1
inst✝¹ : Monoid M
α : Type u_2
inst✝ : MulAction M α
m : Mˣ
x : α
⊢ (fun a => m⁻¹ • a) ((fun a => ↑m • a) x) = x

Proof state:
case intro
M : Type u_1
inst✝¹ : Monoid M
α : Type u_2
inst✝ : MulAction M α
m : Mˣ
⊢ ∃ g, (Function.LeftInverse g fun a => ↑m • a) ∧ Function.RightInverse g fun a => ↑m • a

Tactic:
use fun a ↦ m⁻¹ • a

Result:
case h
M : Type u_1
inst✝¹ : Monoid M
α : Type u_2
inst✝ : MulAction M α
m : Mˣ
⊢ (Function.LeftInverse (fun a => m⁻¹ • a) fun a => ↑m • a) ∧ Function.RightInverse (fun a => m⁻¹ • a) fun a => ↑m • a

Proof state:
case intro
M : Type u_1
inst✝¹ : Monoid M
α : Type u_2
inst✝ : MulAction M α
m : Mˣ
⊢ Function.Bijective fun a => ↑m • a

Tactic:
rw [Function.bijective_iff_has_inverse]

Result:
case intro
M : Type u_1
inst✝¹ : Monoid M
α : Type u_2
inst✝ : MulAction M α
m : Mˣ
⊢ ∃ g, (Function.LeftInverse g fun a => ↑m • a) ∧ Function.RightInverse g fun a => ↑m • a
-- Mathlib/CategoryTheory/Yoneda.lean
lemma coyonedaEquiv_coyoneda_map {X Y : C} (f : X ⟶ Y) :
    coyonedaEquiv (coyoneda.map f.op) = f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ (coyoneda.map f.op).app Y (𝟙 Y) = f

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ coyonedaEquiv (coyoneda.map f.op) = f

Tactic:
rw [coyonedaEquiv_apply]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ (coyoneda.map f.op).app Y (𝟙 Y) = f
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem expand' (r : X) (s s' : S) : r /ₒ s = s' • r /ₒ (s' * s) :=
  OreLocalization.expand r s s' (by norm_cast; apply SetLike.coe_mem)

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s s' : ↥S
⊢ ↑s' * ↑s ∈ S

Tactic:
norm_cast

Result:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s s' : ↥S
⊢ ↑(s' * s) ∈ S

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s s' : ↥S
⊢ ↑(s' * s) ∈ S

Tactic:
apply SetLike.coe_mem

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem infiniteNeg_of_tendsto_bot {f : ℕ → ℝ} (hf : Tendsto f atTop atBot) :
    InfiniteNeg (ofSeq f) := fun r =>
  have hf' := tendsto_atTop_atBot.mp hf
  let ⟨i, hi⟩ := hf' (r - 1)
  have hi' : ∀ a : ℕ, r - 1 < f a → a < i := fun a => lt_imp_lt_of_le_imp_le (hi a)
  have hS : { a : ℕ | f a < r }ᶜ ⊆ { a : ℕ | a ≤ i }

Proof state:
f : ℕ → ℝ
hf : Tendsto f atTop atBot
r : ℝ
hf' : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → f a ≤ b
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → f a ≤ r - 1
hi' : ∀ (a : ℕ), r - 1 < f a → a < i
⊢ {a | f a < r}ᶜ ⊆ {a | a ≤ i}

Tactic:
simp only [Set.compl_setOf, not_lt]

Result:
f : ℕ → ℝ
hf : Tendsto f atTop atBot
r : ℝ
hf' : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → f a ≤ b
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → f a ≤ r - 1
hi' : ∀ (a : ℕ), r - 1 < f a → a < i
⊢ {a | r ≤ f a} ⊆ {a | a ≤ i}

Proof state:
f : ℕ → ℝ
hf : Tendsto f atTop atBot
r : ℝ
hf' : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → f a ≤ b
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → f a ≤ r - 1
hi' : ∀ (a : ℕ), r - 1 < f a → a < i
⊢ {a | r ≤ f a} ⊆ {a | a ≤ i}

Tactic:
exact fun a har => le_of_lt (hi' a (lt_of_lt_of_le (sub_one_lt _) har))

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem two_pow_sub_one_mod_two : (2 ^ n - 1) % 2 = 1 % 2 ^ n

Proof state:
n : Nat
⊢ n + 1 ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
case succ
n : Nat
⊢ (2 ^ (n + 1) - 1) % 2 = 1 % 2 ^ (n + 1)

Tactic:
rw [mod_eq_of_lt (a := 1) (Nat.one_lt_two_pow (by omega)), mod_two_eq_one_iff_testBit_zero, testBit_two_pow_sub_one ]

Result:
case succ
n : Nat
⊢ decide (0 < n + 1) = true

Proof state:
case zero

⊢ (2 ^ 0 - 1) % 2 = 1 % 2 ^ 0

Tactic:
simp

Result:
no goals

Proof state:
case succ
n : Nat
⊢ decide (0 < n + 1) = true

Tactic:
simp only [zero_lt_succ, decide_true]

Result:
no goals

Proof state:
n : Nat
⊢ (2 ^ n - 1) % 2 = 1 % 2 ^ n

Tactic:
cases n with
| zero => simp
| succ n =>
  rw [mod_eq_of_lt (a := 1) (Nat.one_lt_two_pow (by omega)), mod_two_eq_one_iff_testBit_zero, testBit_two_pow_sub_one ]
  simp only [zero_lt_succ, decide_true]

Result:
no goals
-- Mathlib/Data/Nat/GCD/BigOperators.lean
theorem coprime_multiset_prod_right_iff {k : ℕ} {m : Multiset ℕ} :
    Coprime k m.prod ↔ ∀ n ∈ m, Coprime k n

Proof state:
k : ℕ
m : Multiset ℕ
⊢ k.Coprime m.prod ↔ ∀ n ∈ m, k.Coprime n

Tactic:
induction m using Quotient.inductionOn

Result:
case h
k : ℕ
a✝ : List ℕ
⊢ k.Coprime (Multiset.prod ⟦a✝⟧) ↔ ∀ n ∈ ⟦a✝⟧, k.Coprime n

Proof state:
case h
k : ℕ
a✝ : List ℕ
⊢ k.Coprime (Multiset.prod ⟦a✝⟧) ↔ ∀ n ∈ ⟦a✝⟧, k.Coprime n

Tactic:
simpa using coprime_list_prod_right_iff

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem enorm_eq_ofReal_abs (r : ℝ) : ‖r‖ₑ = ENNReal.ofReal |r|

Proof state:
r : ℝ
⊢ ‖r‖ₑ = ENNReal.ofReal |r|

Tactic:
rw [← enorm_eq_ofReal (abs_nonneg _), enorm_abs]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem monoidalPreadditive_of_faithful {D} [Category D] [Preadditive D] [MonoidalCategory D]
    (F : D ⥤ C) [F.Monoidal] [F.Faithful] [F.Additive] :
    MonoidalPreadditive D :=
  { whiskerLeft_zero

Proof state:
C : Type u_1
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
⊢ ∀ {X Y Z : D} (f g : Y ⟶ Z), X ◁ (f + g) = X ◁ f + X ◁ g

Tactic:
intros

Result:
C : Type u_1
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
X✝ Y✝ Z✝ : D
f✝ g✝ : Y✝ ⟶ Z✝
⊢ X✝ ◁ (f✝ + g✝) = X✝ ◁ f✝ + X✝ ◁ g✝
-- Mathlib/ModelTheory/Syntax.lean
theorem comp_onTerm {L'' : Language} (φ : L' →ᴸ L'') (ψ : L →ᴸ L') :
    ((φ.comp ψ).onTerm : L.Term α → L''.Term α) = φ.onTerm ∘ ψ.onTerm

Proof state:
case h
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
t : L.Term α
⊢ (φ.comp ψ).onTerm t = (φ.onTerm ∘ ψ.onTerm) t

Tactic:
induction t with
| var => rfl
| func _ _ ih => simp_rw [onTerm, ih]; rfl

Result:
no goals

Proof state:
case h.func
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), (φ.comp ψ).onTerm (_ts✝ a) = (φ.onTerm ∘ ψ.onTerm) (_ts✝ a)
⊢ (φ.comp ψ).onTerm (func _f✝ _ts✝) = (φ.onTerm ∘ ψ.onTerm) (func _f✝ _ts✝)

Tactic:
simp_rw [onTerm, ih]

Result:
case h.func
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), (φ.comp ψ).onTerm (_ts✝ a) = (φ.onTerm ∘ ψ.onTerm) (_ts✝ a)
⊢ (func ((φ.comp ψ).onFunction _f✝) fun i => (φ.onTerm ∘ ψ.onTerm) (_ts✝ i)) = (φ.onTerm ∘ ψ.onTerm) (func _f✝ _ts✝)

Proof state:
case h.var
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
a✝ : α
⊢ (φ.comp ψ).onTerm (var a✝) = (φ.onTerm ∘ ψ.onTerm) (var a✝)

Tactic:
rfl

Result:
no goals

Proof state:
case h.func
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), (φ.comp ψ).onTerm (_ts✝ a) = (φ.onTerm ∘ ψ.onTerm) (_ts✝ a)
⊢ (func ((φ.comp ψ).onFunction _f✝) fun i => (φ.onTerm ∘ ψ.onTerm) (_ts✝ i)) = (φ.onTerm ∘ ψ.onTerm) (func _f✝ _ts✝)

Tactic:
rfl

Result:
no goals

Proof state:
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
⊢ (φ.comp ψ).onTerm = φ.onTerm ∘ ψ.onTerm

Tactic:
ext t

Result:
case h
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
t : L.Term α
⊢ (φ.comp ψ).onTerm t = (φ.onTerm ∘ ψ.onTerm) t
-- Mathlib/Algebra/Group/Invertible/Defs.lean
theorem mul_invOf_cancel_left' [Monoid α] (a b : α) {_ : Invertible a} : a * (⅟ a * b) = b

Proof state:
α : Type u
inst✝ : Monoid α
a b : α
x✝ : Invertible a
⊢ a * (⅟a * b) = b

Tactic:
rw [← mul_assoc, mul_invOf_self, one_mul]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem cardFactors_eq_one_iff_prime {n : ℕ} : Ω n = 1 ↔ n.Prime

Proof state:
case succ
n : ℕ
h : Ω (n + 1) = 1
⊢ Nat.Prime (n + 1)

Tactic:
rcases List.length_eq_one.1 h with ⟨x, hx⟩

Result:
case succ.intro
n : ℕ
h : Ω (n + 1) = 1
x : ℕ
hx : (n + 1).primeFactorsList = [x]
⊢ Nat.Prime (n + 1)

Proof state:
case succ.intro.a
n : ℕ
h : Ω (n + 1) = 1
x : ℕ
hx : (n + 1).primeFactorsList = [x]
⊢ x ∈ primeFactorsList ?succ.intro.n

case succ.intro.n
n : ℕ
h : Ω (n + 1) = 1
x : ℕ
hx : (n + 1).primeFactorsList = [x]
⊢ ℕ

Tactic:
rw [hx, List.mem_singleton]

Result:
no goals

Proof state:
n : ℕ
⊢ Ω n = 1 ↔ Nat.Prime n

Tactic:
refine ⟨fun h => ?_, fun h => List.length_eq_one.2 ⟨n, primeFactorsList_prime h⟩⟩

Result:
n : ℕ
h : Ω n = 1
⊢ Nat.Prime n

Proof state:
case succ.intro
n : ℕ
h : Ω (n + 1) = 1
x : ℕ
hx : (n + 1).primeFactorsList = [x]
⊢ Nat.Prime (n + 1)

Tactic:
rw [← prod_primeFactorsList n.add_one_ne_zero, hx, List.prod_singleton]

Result:
case succ.intro
n : ℕ
h : Ω (n + 1) = 1
x : ℕ
hx : (n + 1).primeFactorsList = [x]
⊢ Nat.Prime x

Proof state:
n : ℕ
h : Ω n = 1
⊢ Nat.Prime n

Tactic:
cases n with | zero => simp at h | succ n =>
rcases List.length_eq_one.1 h with ⟨x, hx⟩
rw [← prod_primeFactorsList n.add_one_ne_zero, hx, List.prod_singleton]
apply prime_of_mem_primeFactorsList
rw [hx, List.mem_singleton]

Result:
no goals

Proof state:
case zero
h : Ω 0 = 1
⊢ Nat.Prime 0

Tactic:
simp at h

Result:
no goals

Proof state:
case succ.intro
n : ℕ
h : Ω (n + 1) = 1
x : ℕ
hx : (n + 1).primeFactorsList = [x]
⊢ Nat.Prime x

Tactic:
apply prime_of_mem_primeFactorsList

Result:
case succ.intro.a
n : ℕ
h : Ω (n + 1) = 1
x : ℕ
hx : (n + 1).primeFactorsList = [x]
⊢ x ∈ primeFactorsList ?succ.intro.n

case succ.intro.n
n : ℕ
h : Ω (n + 1) = 1
x : ℕ
hx : (n + 1).primeFactorsList = [x]
⊢ ℕ
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem isEquiv_of_val_le_one [LinearOrderedCommGroupWithZero Γ₀]
    [LinearOrderedCommGroupWithZero Γ'₀] {v : Valuation K Γ₀} {v' : Valuation K Γ'₀}
    (h : ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1) : v.IsEquiv v'

Proof state:
case inr
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1
x y : K
hy : y ≠ 0
⊢ v x ≤ v y ↔ v' x ≤ v' y

Tactic:
rw [← div_le_one₀, ← v.map_div, h, v'.map_div, div_le_one₀] <;>
  rwa [zero_lt_iff, ne_zero_iff]

Result:
no goals

Proof state:
case inl
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1
x : K
⊢ v x ≤ v 0 ↔ v' x ≤ v' 0

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1
x y : K
⊢ v x ≤ v y ↔ v' x ≤ v' y

Tactic:
obtain rfl | hy := eq_or_ne y 0

Result:
case inl
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1
x : K
⊢ v x ≤ v 0 ↔ v' x ≤ v' 0

case inr
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1
x y : K
hy : y ≠ 0
⊢ v x ≤ v y ↔ v' x ≤ v' y

Proof state:
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1
⊢ v.IsEquiv v'

Tactic:
intro x y

Result:
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1
x y : K
⊢ v x ≤ v y ↔ v' x ≤ v' y
-- Mathlib/Analysis/Quaternion.lean
theorem coe_real_complex_mul (r : ℝ) (z : ℂ) : (r • z : ℍ) = ↑r * ↑z

Proof state:
r : ℝ
z : ℂ
⊢ r • ↑z = ↑r * ↑z

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/EverywherePos.lean
/-- In a space with an inner regular measure for finite measure sets, any measurable set of finite
measure coincides almost everywhere with its everywhere positive subset. -/
lemma everywherePosSubset_ae_eq_of_measure_ne_top
    [OpensMeasurableSpace α] [InnerRegularCompactLTTop μ] (hs : MeasurableSet s) (h's : μ s ≠ ∞) :
    μ.everywherePosSubset s =ᵐ[μ] s

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ⊤
A : μ (s \ μ.everywherePosSubset s) ≠ ⊤
⊢ ∀ i ⊆ s \ μ.everywherePosSubset s, IsCompact i → μ i = 0

Tactic:
intro k hk h'k

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ⊤
A : μ (s \ μ.everywherePosSubset s) ≠ ⊤
k : Set α
hk : k ⊆ s \ μ.everywherePosSubset s
h'k : IsCompact k
⊢ μ k = 0

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ⊤
A : μ (s \ μ.everywherePosSubset s) ≠ ⊤
⊢ μ.everywherePosSubset s =ᶠ[ae μ] s

Tactic:
simp only [ae_eq_set, diff_eq_empty.mpr (everywherePosSubset_subset μ s), measure_empty,
  true_and, (hs.diff hs.everywherePosSubset).measure_eq_iSup_isCompact_of_ne_top A,
  ENNReal.iSup_eq_zero]

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ⊤
A : μ (s \ μ.everywherePosSubset s) ≠ ⊤
⊢ ∀ i ⊆ s \ μ.everywherePosSubset s, IsCompact i → μ i = 0

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ⊤
⊢ μ.everywherePosSubset s =ᶠ[ae μ] s

Tactic:
have A : μ (s \ μ.everywherePosSubset s) ≠ ∞ :=
  ((measure_mono diff_subset).trans_lt h's.lt_top).ne

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ⊤
A : μ (s \ μ.everywherePosSubset s) ≠ ⊤
⊢ μ.everywherePosSubset s =ᶠ[ae μ] s

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ⊤
A : μ (s \ μ.everywherePosSubset s) ≠ ⊤
k : Set α
hk : k ⊆ s \ μ.everywherePosSubset s
h'k : IsCompact k
⊢ μ k = 0

Tactic:
exact measure_eq_zero_of_subset_diff_everywherePosSubset h'k hk

Result:
no goals