harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/MvPowerSeries/Trunc.lean
theorem trunc'_C_mul (n : σ →₀ ℕ) (a : R) (p : MvPowerSeries σ R) :
    trunc' R n (C σ R a * p) = MvPolynomial.C a * trunc' R n p

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
p : MvPowerSeries σ R
⊢ (trunc' R n) ((C σ R) a * p) = MvPolynomial.C a * (trunc' R n) p

Tactic:
ext m

Result:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
p : MvPowerSeries σ R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc' R n) ((C σ R) a * p)) = MvPolynomial.coeff m (MvPolynomial.C a * (trunc' R n) p)

Proof state:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
p : MvPowerSeries σ R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc' R n) ((C σ R) a * p)) = MvPolynomial.coeff m (MvPolynomial.C a * (trunc' R n) p)

Tactic:
simp [coeff_trunc']

Result:
no goals
-- Mathlib/Data/List/Sym.lean
theorem Subperm.sym2 {xs ys : List α} (h : xs <+~ ys) : xs.sym2 <+~ ys.sym2

Proof state:
α : Type u_1
xs ys : List α
h : xs <+~ ys
⊢ xs.sym2 <+~ ys.sym2

Tactic:
obtain ⟨xs', hx, h⟩ := h

Result:
case intro.intro
α : Type u_1
xs ys xs' : List α
hx : xs' ~ xs
h : xs' <+ ys
⊢ xs.sym2 <+~ ys.sym2

Proof state:
case intro.intro
α : Type u_1
xs ys xs' : List α
hx : xs' ~ xs
h : xs' <+ ys
⊢ xs.sym2 <+~ ys.sym2

Tactic:
exact hx.sym2.symm.subperm.trans h.sym2.subperm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem bmod_add_mul_cancel (x : Int) (n : Nat) (k : Int) : Int.bmod (x + n * k) n = Int.bmod x n

Proof state:
x : Int
n : Nat
k : Int
⊢ (x + ↑n * k).bmod n = x.bmod n

Tactic:
simp [bmod_def]

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Lemmas.lean
theorem minimalPeriod_snd_dvd : minimalPeriod g x.2 ∣ minimalPeriod (Prod.map f g) x

Proof state:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
⊢ minimalPeriod g x.2 ∣ minimalPeriod (Prod.map f g) x

Tactic:
rw [minimalPeriod_prod_map]

Result:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
⊢ minimalPeriod g x.2 ∣ (minimalPeriod f x.1).lcm (minimalPeriod g x.2)

Proof state:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
⊢ minimalPeriod g x.2 ∣ (minimalPeriod f x.1).lcm (minimalPeriod g x.2)

Tactic:
exact Nat.dvd_lcm_right _ _

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem toList_map {β : Type*} (v : Vector α n) (f : α → β) :
    (v.map f).toList = v.toList.map f

Proof state:
case mk
α : Type u_1
n : ℕ
β : Type u_6
f : α → β
val✝ : List α
property✝ : val✝.length = n
⊢ (map f ⟨val✝, property✝⟩).toList = List.map f (toList ⟨val✝, property✝⟩)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α n
f : α → β
⊢ (map f v).toList = List.map f v.toList

Tactic:
cases v

Result:
case mk
α : Type u_1
n : ℕ
β : Type u_6
f : α → β
val✝ : List α
property✝ : val✝.length = n
⊢ (map f ⟨val✝, property✝⟩).toList = List.map f (toList ⟨val✝, property✝⟩)
-- Mathlib/GroupTheory/PGroup.lean
theorem bot_lt_center [Nontrivial G] [Finite G] : ⊥ < Subgroup.center G

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : Nontrivial ↥(Subgroup.center G)
⊢ ⊥ < Subgroup.center G

Tactic:
classical exact
    bot_lt_iff_ne_bot.mpr ((Subgroup.center G).one_lt_card_iff_ne_bot.mp Finite.one_lt_card)

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
⊢ ⊥ < Subgroup.center G

Tactic:
haveI := center_nontrivial hG

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : Nontrivial ↥(Subgroup.center G)
⊢ ⊥ < Subgroup.center G

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : Nontrivial ↥(Subgroup.center G)
⊢ ⊥ < Subgroup.center G

Tactic:
exact
bot_lt_iff_ne_bot.mpr ((Subgroup.center G).one_lt_card_iff_ne_bot.mp Finite.one_lt_card)

Result:
no goals
-- Mathlib/Data/Set/List.lean
theorem range_list_map (f : α → β) : range (map f) = { l | ∀ x ∈ l, x ∈ range f }

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ range (map f) = {l | ∀ x ∈ l, x ∈ range f}

Tactic:
refine antisymm (range_subset_iff.2 fun l => forall_mem_map.2 fun y _ => mem_range_self _)
    fun l hl => ?_

Result:
α : Type u_1
β : Type u_2
f : α → β
l : List β
hl : l ∈ {l | ∀ x ∈ l, x ∈ range f}
⊢ l ∈ range (map f)

Proof state:
case cons.intro.intro
α : Type u_1
β : Type u_2
f : α → β
l : List α
ihl : map f l ∈ {l | ∀ x ∈ l, x ∈ range f} → map f l ∈ range (map f)
a : α
hl : f a :: map f l ∈ {l | ∀ x ∈ l, x ∈ range f}
⊢ f a :: map f l ∈ range (map f)

Tactic:
exact ⟨a :: l, map_cons _ _ _⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List β
hl : l ∈ {l | ∀ x ∈ l, x ∈ range f}
⊢ l ∈ range (map f)

Tactic:
induction l with
| nil => exact ⟨[], rfl⟩
| cons a l ihl =>
  rcases ihl fun x hx => hl x <| subset_cons_self _ _ hx with ⟨l, rfl⟩
  rcases hl a (mem_cons_self _ _) with ⟨a, rfl⟩
  exact ⟨a :: l, map_cons _ _ _⟩

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → β
hl : [] ∈ {l | ∀ x ∈ l, x ∈ range f}
⊢ [] ∈ range (map f)

Tactic:
exact ⟨[], rfl⟩

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
a : β
l : List β
ihl : l ∈ {l | ∀ x ∈ l, x ∈ range f} → l ∈ range (map f)
hl : a :: l ∈ {l | ∀ x ∈ l, x ∈ range f}
⊢ a :: l ∈ range (map f)

Tactic:
rcases ihl fun x hx => hl x <| subset_cons_self _ _ hx with ⟨l, rfl⟩

Result:
case cons.intro
α : Type u_1
β : Type u_2
f : α → β
a : β
l : List α
ihl : map f l ∈ {l | ∀ x ∈ l, x ∈ range f} → map f l ∈ range (map f)
hl : a :: map f l ∈ {l | ∀ x ∈ l, x ∈ range f}
⊢ a :: map f l ∈ range (map f)

Proof state:
case cons.intro
α : Type u_1
β : Type u_2
f : α → β
a : β
l : List α
ihl : map f l ∈ {l | ∀ x ∈ l, x ∈ range f} → map f l ∈ range (map f)
hl : a :: map f l ∈ {l | ∀ x ∈ l, x ∈ range f}
⊢ a :: map f l ∈ range (map f)

Tactic:
rcases hl a (mem_cons_self _ _) with ⟨a, rfl⟩

Result:
case cons.intro.intro
α : Type u_1
β : Type u_2
f : α → β
l : List α
ihl : map f l ∈ {l | ∀ x ∈ l, x ∈ range f} → map f l ∈ range (map f)
a : α
hl : f a :: map f l ∈ {l | ∀ x ∈ l, x ∈ range f}
⊢ f a :: map f l ∈ range (map f)
-- Mathlib/MeasureTheory/Function/LpSpace/DomAct/Basic.lean
theorem edist_smul_Lp (c : Mᵈᵐᵃ) (f g : Lp E p μ) : edist (c • f) (c • g) = edist f g

Proof state:
M : Type u_1
α : Type u_3
E : Type u_4
inst✝⁵ : MeasurableSpace M
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableSMul M α
c : Mᵈᵐᵃ
f g : ↥(Lp E p μ)
⊢ edist (c • f) (c • g) = edist f g

Tactic:
simp only [Lp.edist_dist, dist_smul_Lp]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Defs.lean
theorem mem_orbit_smul (g : G) (a : α) : a ∈ orbit G (g • a)

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ a ∈ orbit G (g • a)

Tactic:
simp only [orbit_smul, mem_orbit_self]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_insert_of_eq_one_if_not_mem [DecidableEq α] (h : a ∉ s → f a = 1) :
    ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x

Proof state:
case neg
α : Type u_3
β : Type u_4
s : Finset α
a : α
f : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
h : a ∉ s → f a = 1
hm : a ∉ s
⊢ ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x

Tactic:
rw [prod_insert hm, h hm, one_mul]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
a : α
f : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
h : a ∉ s → f a = 1
⊢ ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x

Tactic:
by_cases hm : a ∈ s

Result:
case pos
α : Type u_3
β : Type u_4
s : Finset α
a : α
f : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
h : a ∉ s → f a = 1
hm : a ∈ s
⊢ ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x

case neg
α : Type u_3
β : Type u_4
s : Finset α
a : α
f : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
h : a ∉ s → f a = 1
hm : a ∉ s
⊢ ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x

Proof state:
case pos
α : Type u_3
β : Type u_4
s : Finset α
a : α
f : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
h : a ∉ s → f a = 1
hm : a ∈ s
⊢ ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x

Tactic:
simp_rw [insert_eq_of_mem hm]

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem diff_union_inter (s t : Set α) : s \ t ∪ s ∩ t = s

Proof state:
α : Type u
s t : Set α
⊢ s ∩ t ∪ s \ t = s

Tactic:
exact sup_inf_sdiff _ _

Result:
no goals

Proof state:
α : Type u
s t : Set α
⊢ s \ t ∪ s ∩ t = s

Tactic:
rw [union_comm]

Result:
α : Type u
s t : Set α
⊢ s ∩ t ∪ s \ t = s
-- Mathlib/LinearAlgebra/Semisimple.lean
lemma IsSemisimple_smul (t : K) (h : f.IsSemisimple) :
    (t • f).IsSemisimple

Proof state:
case inr
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
t : K
h : f.IsSemisimple
this :
  ∀ {M : Type u_2} [inst : AddCommGroup M] {K : Type u_3} [inst_1 : Field K] [inst_2 : Module K M] {f : End K M}
    (t : K), f.IsSemisimple → t ≠ 0 → (t • f).IsSemisimple
ht : ¬t ≠ 0
⊢ (t • f).IsSemisimple

Tactic:
simp [not_not.mp ht]

Result:
no goals

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
t : K
h : f.IsSemisimple
⊢ (t • f).IsSemisimple

Tactic:
wlog ht : t ≠ 0

Result:
case inr
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
t : K
h : f.IsSemisimple
this :
  ∀ {M : Type u_2} [inst : AddCommGroup M] {K : Type u_3} [inst_1 : Field K] [inst_2 : Module K M] {f : End K M}
    (t : K), f.IsSemisimple → t ≠ 0 → (t • f).IsSemisimple
ht : ¬t ≠ 0
⊢ (t • f).IsSemisimple

M✝ : Type u_2
inst✝⁵ : AddCommGroup M✝
K✝ : Type u_3
inst✝⁴ : Field K✝
inst✝³ : Module K✝ M✝
f✝ : End K✝ M✝
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
t : K
h : f.IsSemisimple
ht : t ≠ 0
⊢ (t • f).IsSemisimple

Proof state:
M✝ : Type u_2
inst✝⁵ : AddCommGroup M✝
K✝ : Type u_3
inst✝⁴ : Field K✝
inst✝³ : Module K✝ M✝
f✝ : End K✝ M✝
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
t : K
h : f.IsSemisimple
ht : t ≠ 0
⊢ (t • f).IsSemisimple

Tactic:
rwa [IsSemisimple_smul_iff ht]

Result:
no goals
-- Mathlib/Data/List/Flatten.lean
theorem Sublist.flatten {l₁ l₂ : List (List α)} (h : l₁ <+ l₂) :
    l₁.flatten <+ l₂.flatten

Proof state:
α : Type u_1
l₁ l₂ : List (List α)
h : l₁ <+ l₂
⊢ l₁.flatten <+ l₂.flatten

Tactic:
induction h with
| slnil => simp
| cons _ _ ih =>
  rw [flatten_cons]
  exact ih.trans (sublist_append_right _ _)
| cons₂ _ _ ih => simpa

Result:
no goals

Proof state:
case cons₂
α : Type u_1
l₁ l₂ l₁✝ l₂✝ : List (List α)
a✝¹ : List α
a✝ : l₁✝ <+ l₂✝
ih : l₁✝.flatten <+ l₂✝.flatten
⊢ (a✝¹ :: l₁✝).flatten <+ (a✝¹ :: l₂✝).flatten

Tactic:
simpa

Result:
no goals

Proof state:
case slnil
α : Type u_1
l₁ l₂ : List (List α)
⊢ [].flatten <+ [].flatten

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
l₁ l₂ l₁✝ l₂✝ : List (List α)
a✝¹ : List α
a✝ : l₁✝ <+ l₂✝
ih : l₁✝.flatten <+ l₂✝.flatten
⊢ l₁✝.flatten <+ (a✝¹ :: l₂✝).flatten

Tactic:
rw [flatten_cons]

Result:
case cons
α : Type u_1
l₁ l₂ l₁✝ l₂✝ : List (List α)
a✝¹ : List α
a✝ : l₁✝ <+ l₂✝
ih : l₁✝.flatten <+ l₂✝.flatten
⊢ l₁✝.flatten <+ a✝¹ ++ l₂✝.flatten

Proof state:
case cons
α : Type u_1
l₁ l₂ l₁✝ l₂✝ : List (List α)
a✝¹ : List α
a✝ : l₁✝ <+ l₂✝
ih : l₁✝.flatten <+ l₂✝.flatten
⊢ l₁✝.flatten <+ a✝¹ ++ l₂✝.flatten

Tactic:
exact ih.trans (sublist_append_right _ _)

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem nnnorm_equiv (f : PiLp ∞ β) : ‖WithLp.equiv ⊤ _ f‖₊ = ‖f‖₊

Proof state:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ⊤ β
⊢ ⨆ i, ‖(WithLp.equiv ⊤ ((i : ι) → β i)) f i‖₊ = ⨆ i, ‖f i‖₊

Tactic:
dsimp only [WithLp.equiv_pi_apply]

Result:
no goals

Proof state:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ⊤ β
⊢ ‖(WithLp.equiv ⊤ ((i : ι) → β i)) f‖₊ = ‖f‖₊

Tactic:
rw [nnnorm_eq_ciSup, Pi.nnnorm_def, Finset.sup_univ_eq_ciSup]

Result:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ⊤ β
⊢ ⨆ i, ‖(WithLp.equiv ⊤ ((i : ι) → β i)) f i‖₊ = ⨆ i, ‖f i‖₊
-- Mathlib/CategoryTheory/Monad/Basic.lean
lemma map_counit_app (T : Comonad C) (X : C) [IsIso T.δ] :
    T.map (T.ε.app X) = T.ε.app (T.obj X)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Comonad C
X : C
inst✝ : IsIso T.δ
⊢ T.map (T.ε.app X) = T.ε.app (T.obj X)

Tactic:
simp [← cancel_epi (T.δ.app _)]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Raised.right {l x₁ x₂ r₁ r₂} (H : Raised (size r₁) (size r₂)) :
    Raised (size (@node' α l x₁ r₁)) (size (@node' α l x₂ r₂))

Proof state:
case inr
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
⊢ Raised (l.size + r₁.size + 1) (l.size + (r₁.size + 1) + 1)

Tactic:
exact Or.inr rfl

Result:
no goals

Proof state:
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
m : ℕ
H : Raised r₁.size m
⊢ Raised (l.size + r₁.size + 1) (l.size + m + 1)

Tactic:
rcases H with (rfl | rfl)

Result:
case inl
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
⊢ Raised (l.size + r₁.size + 1) (l.size + r₁.size + 1)

case inr
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
⊢ Raised (l.size + r₁.size + 1) (l.size + (r₁.size + 1) + 1)

Proof state:
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
H : Raised r₁.size r₂.size
⊢ Raised (l.size + r₁.size + 1) (l.size + r₂.size + 1)

Tactic:
generalize size r₂ = m at H ⊢

Result:
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
m : ℕ
H : Raised r₁.size m
⊢ Raised (l.size + r₁.size + 1) (l.size + m + 1)

Proof state:
case inl
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
⊢ Raised (l.size + r₁.size + 1) (l.size + r₁.size + 1)

Tactic:
exact Or.inl rfl

Result:
no goals

Proof state:
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
H : Raised r₁.size r₂.size
⊢ Raised (l.node' x₁ r₁).size (l.node' x₂ r₂).size

Tactic:
rw [node', size_node, size_node]

Result:
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
H : Raised r₁.size r₂.size
⊢ Raised (l.size + r₁.size + 1) (l.size + r₂.size + 1)
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_sdiff_eq_sup : a ∆ (b \ a) = a ⊔ b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ (b \ a) ⊔ b \ a = a ⊔ b

Tactic:
exact
  le_antisymm (sup_le_sup sdiff_le sdiff_le)
    (sup_le le_sdiff_sup <| le_sdiff_sup.trans <| sup_le le_sup_right le_sdiff_sup)

Result:
no goals

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ (b \ a) = a ⊔ b

Tactic:
rw [symmDiff, sdiff_idem]

Result:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ (b \ a) ⊔ b \ a = a ⊔ b
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem HasCoseparator.hasSeparator_of_hasCoseparator_op [HasCoseparator Cᵒᵖ] :
    HasSeparator C

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasCoseparator Cᵒᵖ
⊢ HasSeparator C

Tactic:
simp_all

Result:
no goals
-- Mathlib/GroupTheory/Coset/Basic.lean
theorem mem_leftCoset_iff (a : α) : x ∈ a • s ↔ a⁻¹ * x ∈ s :=
  Iff.intro (fun ⟨b, hb, Eq⟩ => by simp [Eq.symm, hb]) fun h => ⟨a⁻¹ * x, h, by simp⟩

Proof state:
α : Type u_1
inst✝ : Group α
s : Set α
x a : α
h : a⁻¹ * x ∈ s
⊢ (fun x => a • x) (a⁻¹ * x) = x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Group α
s : Set α
x a : α
x✝ : x ∈ a • s
b : α
hb : b ∈ s
Eq : (fun x => a • x) b = x
⊢ a⁻¹ * x ∈ s

Tactic:
simp [Eq.symm, hb]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem comap_eval_neBot_iff {ι : Type*} {α : ι → Type*} [∀ j, Nonempty (α j)] {i : ι}
    {f : Filter (α i)} : (comap (eval i) f).NeBot ↔ NeBot f

Proof state:
ι : Type u_6
α : ι → Type u_7
inst✝ : ∀ (j : ι), Nonempty (α j)
i : ι
f : Filter (α i)
⊢ (comap (eval i) f).NeBot ↔ f.NeBot

Tactic:
simp [comap_eval_neBot_iff', *]

Result:
no goals
-- Mathlib/MeasureTheory/Function/Jacobian.lean
theorem det_one_smulRight {𝕜 : Type*} [CommRing 𝕜] [TopologicalSpace 𝕜] [ContinuousMul 𝕜] (v : 𝕜) :
    ((1 : 𝕜 →L[𝕜] 𝕜).smulRight v).det = v

Proof state:
𝕜 : Type u_3
inst✝² : CommRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousMul 𝕜
v : 𝕜
a✝ : Nontrivial 𝕜
this : ContinuousLinearMap.smulRight 1 v = v • 1
⊢ (ContinuousLinearMap.smulRight 1 v).det = v

Tactic:
rw [this, ContinuousLinearMap.det, ContinuousLinearMap.coe_smul,
  ContinuousLinearMap.one_def, ContinuousLinearMap.coe_id, LinearMap.det_smul,
  Module.finrank_self, LinearMap.det_id, pow_one, mul_one]

Result:
no goals

Proof state:
𝕜 : Type u_3
inst✝² : CommRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousMul 𝕜
v : 𝕜
⊢ (ContinuousLinearMap.smulRight 1 v).det = v

Tactic:
nontriviality 𝕜

Result:
𝕜 : Type u_3
inst✝² : CommRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousMul 𝕜
v : 𝕜
a✝ : Nontrivial 𝕜
⊢ (ContinuousLinearMap.smulRight 1 v).det = v

Proof state:
case h
𝕜 : Type u_3
inst✝² : CommRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousMul 𝕜
v : 𝕜
a✝ : Nontrivial 𝕜
⊢ (ContinuousLinearMap.smulRight 1 v) 1 = (v • 1) 1

Tactic:
simp only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply,
  Algebra.id.smul_eq_mul, one_mul, ContinuousLinearMap.coe_smul', Pi.smul_apply, mul_one]

Result:
no goals

Proof state:
𝕜 : Type u_3
inst✝² : CommRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousMul 𝕜
v : 𝕜
a✝ : Nontrivial 𝕜
⊢ (ContinuousLinearMap.smulRight 1 v).det = v

Tactic:
have : (1 : 𝕜 →L[𝕜] 𝕜).smulRight v = v • (1 : 𝕜 →L[𝕜] 𝕜) := by
  ext1
  simp only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply,
    Algebra.id.smul_eq_mul, one_mul, ContinuousLinearMap.coe_smul', Pi.smul_apply, mul_one]

Result:
𝕜 : Type u_3
inst✝² : CommRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousMul 𝕜
v : 𝕜
a✝ : Nontrivial 𝕜
this : ContinuousLinearMap.smulRight 1 v = v • 1
⊢ (ContinuousLinearMap.smulRight 1 v).det = v

Proof state:
𝕜 : Type u_3
inst✝² : CommRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousMul 𝕜
v : 𝕜
a✝ : Nontrivial 𝕜
⊢ ContinuousLinearMap.smulRight 1 v = v • 1

Tactic:
ext1

Result:
case h
𝕜 : Type u_3
inst✝² : CommRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousMul 𝕜
v : 𝕜
a✝ : Nontrivial 𝕜
⊢ (ContinuousLinearMap.smulRight 1 v) 1 = (v • 1) 1
-- Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean
lemma prod_norm_sq (x : C⋆ᵐᵒᵈ (E × F)) : ‖x‖ ^ 2 = ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

Proof state:
A : Type u_1
inst✝⁹ : NonUnitalCStarAlgebra A
inst✝⁸ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : Module ℂ E
inst✝⁵ : SMul Aᵐᵒᵖ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : Module ℂ F
inst✝² : SMul Aᵐᵒᵖ F
inst✝¹ : CStarModule A E
inst✝ : CStarModule A F
x : C⋆ᵐᵒᵈ (E × F)
⊢ ‖x‖ ^ 2 = ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

Tactic:
simp [prod_norm]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem apply_lt_nfpBFamily_iff (ho : o ≠ 0) (H : ∀ i hi, IsNormal (f i hi)) {a b} :
    (∀ i hi, f i hi b < nfpBFamily.{u, v} o f a) ↔ b < nfpBFamily.{u, v} o f a :=
  ⟨fun h => by
    haveI := toType_nonempty_iff_ne_zero.2 ho
    refine (apply_lt_nfpFamily_iff ?_).1 fun _ => h _ _
    exact fun _ => H _ _, apply_lt_nfpBFamily H⟩

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a b : Ordinal.{max u v}
h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi b < o.nfpBFamily f a
this : Nonempty o.toType
⊢ ∀ (i : o.toType), IsNormal (o.familyOfBFamily f i)

Tactic:
exact fun _ => H _ _

Result:
no goals

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a b : Ordinal.{max u v}
h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi b < o.nfpBFamily f a
this : Nonempty o.toType
⊢ b < o.nfpBFamily f a

Tactic:
refine (apply_lt_nfpFamily_iff ?_).1 fun _ => h _ _

Result:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a b : Ordinal.{max u v}
h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi b < o.nfpBFamily f a
this : Nonempty o.toType
⊢ ∀ (i : o.toType), IsNormal (o.familyOfBFamily f i)

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a b : Ordinal.{max u v}
h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi b < o.nfpBFamily f a
⊢ b < o.nfpBFamily f a

Tactic:
haveI := toType_nonempty_iff_ne_zero.2 ho

Result:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
ho : o ≠ 0
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a b : Ordinal.{max u v}
h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi b < o.nfpBFamily f a
this : Nonempty o.toType
⊢ b < o.nfpBFamily f a
-- Mathlib/Logic/Equiv/Basic.lean
theorem piCongr'_symm_apply_symm_apply (f : ∀ b, Z b) (b : β) :
    (h₁.piCongr' h₂).symm f (h₁.symm b) = (h₂ b).symm (f b)

Proof state:
α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (h₁.symm b) ≃ Z b
f : (b : β) → Z b
b : β
⊢ (h₁.piCongr' h₂).symm f (h₁.symm b) = (h₂ b).symm (f b)

Tactic:
simp [piCongr', piCongr_apply_apply]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiff_one_iff_fderiv :
    ContDiff 𝕜 1 f ↔ Differentiable 𝕜 f ∧ Continuous (fderiv 𝕜 f)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
⊢ Differentiable 𝕜 f ∧ (0 = ω → AnalyticOnNhd 𝕜 f univ) ∧ ContDiff 𝕜 0 (fderiv 𝕜 f) ↔
    Differentiable 𝕜 f ∧ Continuous (fderiv 𝕜 f)

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
⊢ ContDiff 𝕜 1 f ↔ Differentiable 𝕜 f ∧ Continuous (fderiv 𝕜 f)

Tactic:
rw [← zero_add 1, contDiff_succ_iff_fderiv]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
⊢ Differentiable 𝕜 f ∧ (0 = ω → AnalyticOnNhd 𝕜 f univ) ∧ ContDiff 𝕜 0 (fderiv 𝕜 f) ↔
    Differentiable 𝕜 f ∧ Continuous (fderiv 𝕜 f)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem div_eq_of_lt (h₀ : a < b) : a / b = 0

Proof state:
case hnc
a b : Nat
h₀ : a < b
⊢ ¬(0 < b ∧ b ≤ a)

Tactic:
intro h₁

Result:
case hnc
a b : Nat
h₀ : a < b
h₁ : 0 < b ∧ b ≤ a
⊢ False

Proof state:
case hnc
a b : Nat
h₀ : a < b
h₁ : 0 < b ∧ b ≤ a
⊢ False

Tactic:
apply Nat.not_le_of_gt h₀ h₁.right

Result:
no goals

Proof state:
a b : Nat
h₀ : a < b
⊢ a / b = 0

Tactic:
rw [div_eq a, if_neg]

Result:
case hnc
a b : Nat
h₀ : a < b
⊢ ¬(0 < b ∧ b ≤ a)
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma XIsoOfEq_hom_comp_XIsoOfEq_hom (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι}
    (h₁₂ : p₁ = p₂) (h₂₃ : p₂ = p₃) :
    (K.XIsoOfEq h₁₂).hom ≫ (K.XIsoOfEq h₂₃).hom = (K.XIsoOfEq (h₁₂.trans h₂₃)).hom

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₁₂ : p₁ = p₂
h₂₃ : p₂ = p₃
⊢ (K.XIsoOfEq h₁₂).hom ≫ (K.XIsoOfEq h₂₃).hom = (K.XIsoOfEq ⋯).hom

Tactic:
dsimp [XIsoOfEq]

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₁₂ : p₁ = p₂
h₂₃ : p₂ = p₃
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = eqToHom ⋯

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₁₂ : p₁ = p₂
h₂₃ : p₂ = p₃
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = eqToHom ⋯

Tactic:
simp only [eqToHom_trans]

Result:
no goals