mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case pos
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
h :
  (∀ (i : ι), i ∈ s ∧ g i ≤ f i → (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ (i : ι), i ∈ s ∧ f i < g i → (if g i ≤ f i then f i - g i else g i - f i) = 0
i : ι
hi : i ∈ s
hi' : g i ≤ f i
⊢ f i = g i

Tactic:
apply hi'.antisymm'

Goal state after:
case pos
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := ⋯
this : OrderedSub R
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
h :
  (∀ (i : ι), i ∈ s ∧ g i ≤ f i → (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ (i : ι), i ∈ s ∧ f i < g i → (if g i ≤ f i then f i - g i else g i - f i) = 0
i : ι
hi : i ∈ s
hi' : g i ≤ f i
⊢ f i ≤ g i
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: case inr.inr.inl
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
b_0 : card β < 1
⊢ card (α → β) = card β ^ ⊤

Tactic:
rw [Order.lt_one_iff, card_eq_zero_iff_empty] at b_0

Goal state after:
case inr.inr.inl
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
b_0 : IsEmpty β
⊢ card (α → β) = card β ^ ⊤
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M ≤ ↑n
⊢ ↑n < ℵ₀

Tactic:
exact natCast_lt_aleph0

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ ↑n < ℵ₀

Tactic:
exact natCast_lt_aleph0

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: case hc
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ ↑n < ℵ₀

Tactic:
exact natCast_lt_aleph0

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ : Nontrivial R
x✝ : ∃ f, Injective ⇑f
f : (Fin 2 → R) →ₗ[R] R
inj : Injective ⇑f
⊢ f ![0, 1] • f ![1, 0] = f ![1, 0] • f ![0, 1]

Tactic:
smul_eq_mul

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ : Nontrivial R
x✝ : ∃ f, Injective ⇑f
f : (Fin 2 → R) →ₗ[R] R
inj : Injective ⇑f
⊢ f ![0, 1] * f ![1, 0] = f ![1, 0] * f ![0, 1]
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ : Nontrivial R
x✝ : ∃ f, Injective ⇑f
f : (Fin 2 → R) →ₗ[R] R
inj : Injective ⇑f
this : f ![0, 1] • ![1, 0] = f ![1, 0] • ![0, 1]
⊢ False

Tactic:
have h₁ : f ![0, 1] = 0 := by simpa using congr($this 0)

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ : Nontrivial R
x✝ : ∃ f, Injective ⇑f
f : (Fin 2 → R) →ₗ[R] R
inj : Injective ⇑f
this : f ![0, 1] • ![1, 0] = f ![1, 0] • ![0, 1]
h₁ : f ![0, 1] = 0
⊢ False
Module: Mathlib.Algebra.EuclideanDomain.Int

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
⊢ a.natAbs ≤ (a * b).natAbs

Tactic:
rw [← mul_one a.natAbs, Int.natAbs_mul]
        rw [← Int.natAbs_pos] at b0
        exact Nat.mul_le_mul_left _ b0

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
f g : ι → R
⊢ (∑ x ∈ s, (f x • v x - g x • v x) = 0 → ∀ i ∈ s, f i = g i) ↔ ∑ i ∈ s, (f - g) i • v i = 0 → ∀ i ∈ s, (f - g) i = 0

Tactic:
simp only [Pi.sub_apply, sub_smul, sub_eq_zero]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : k = ⊤
hkt : k ≤ t.encard
hs : s.encard = ⊤
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k

Tactic:
subst hsk

Goal state after:
case inl
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard = ⊤
hkt : ⊤ ≤ t.encard
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = ⊤
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: case succ
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
n : ℕ
rank_ih : (N : Submodule R M) → (∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n) → P N
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n + 1
N' : Submodule R M
N'_le : N' ≤ N
x : M
x_mem : x ∈ N
x_ortho : ∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0
m : ℕ
v : Fin m → ↥N'
hli : LinearIndependent R (Subtype.val ∘ v)
c : R
y : M
hy : y ∈ span R (range (Subtype.val ∘ v))
⊢ c • x + y = 0 → c = 0

Tactic:
hc

Goal state after:
case succ
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
n : ℕ
rank_ih : (N : Submodule R M) → (∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n) → P N
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n + 1
N' : Submodule R M
N'_le : N' ≤ N
x : M
x_mem : x ∈ N
x_ortho : ∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0
m : ℕ
v : Fin m → ↥N'
hli : LinearIndependent R (Subtype.val ∘ v)
c : R
y : M
hy : y ∈ span R (range (Subtype.val ∘ v))
hc : c • x + y = 0
⊢ c = 0
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Type u_3
inst✝ : Group H
K : Subgroup G
f : G →* H
hf : Function.Injective ⇑f
⊢ Nat.card ↥(map f K) = Nat.card ↥K

Tactic:
by
  apply Nat.card_image_of_injective hf

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a : α
s : Set α
h : s.Finite
⊢ s.ncard ≤ (insert a s).ncard

Tactic:
ncard_insert_eq_ite h

Goal state after:
α : Type u_1
a : α
s : Set α
h : s.Finite
⊢ s.ncard ≤ if a ∈ s then s.ncard else s.ncard + 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f x ⋯ = f y ⋯
⊢ x = y

Tactic:
exact h₂ _ _ hx hy hxy

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a b : ↥s
⊢ a⁻¹ * b ∈ H.subgroupOf s → ((inclusion h) a)⁻¹ * (inclusion h) b ∈ H.subgroupOf t

Tactic:
exact id

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
H : Subgroup α
⊢ ∀ (a₁ a₂ : ↥H), (∀ (x : ι), a₁⁻¹ * a₂ ∈ (f x).subgroupOf H) → a₁⁻¹ * a₂ ∈ (⨅ i, f i).subgroupOf H

Tactic:
mem_subgroupOf,

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
H : Subgroup α
⊢ ∀ (a₁ a₂ : ↥H), (∀ (x : ι), ↑(a₁⁻¹ * a₂) ∈ f x) → ↑(a₁⁻¹ * a₂) ∈ ⨅ i, f i
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (j : Fin (n + 1)) → Group (α j)
i : Fin (n + 1)
x y : α i
p : (j : Fin n) → α (i.succAbove j)
⊢ (i.insertNth (x / y) fun i_1 ↦ 1) = i.insertNth (x / y) 1

Tactic:
Pi.one_def

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
s : Set α
⊢ sᶜ = ∅ ↔ s.ncard = Nat.card α

Tactic:
← ncard_eq_zero,

Goal state after:
α : Type u_1
inst✝ : Finite α
s : Set α
⊢ sᶜ.ncard = 0 ↔ s.ncard = Nat.card α
Module: Mathlib.Algebra.Algebra.Prod

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
⊢ ∀ (r : R) (x : A × B), r • x = ((algebraMap R A).prod (algebraMap R B)) r * x

Tactic:
rintro r ⟨a, b⟩
    dsimp
    rw [Algebra.smul_def r a, Algebra.smul_def r b]

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: H : Type u_2
I : Type u_3
inst✝¹ : Monoid H
inst✝ : Monoid I
G : Submonoid (H × I)
hG₁ : Bijective (Prod.fst ∘ ⇑G.subtype)
⊢ ∃ f, G = f.mgraph

Tactic:
by
  simpa using MonoidHom.exists_mrange_eq_mgraph hG₁.surjective
    fun a b h ↦ congr_arg (Prod.snd ∘ G.subtype) (hG₁.injective h)

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr.refine_1
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

Tactic:
by_cases ha : a ∈ Set.range g <;> by_cases hb : b ∈ Set.range g <;> grind

Goal state after:
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝³ : Finite ι
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsCodirectedOrder α
f : ι → α
⊢ BddBelow (Set.range f)

Tactic:
obtain ⟨M, hM⟩ := Finite.exists_ge f

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝³ : Finite ι
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsCodirectedOrder α
f : ι → α
M : α
hM : ∀ (i : ι), M ≤ f i
⊢ BddBelow (Set.range f)
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case pos.refine_2
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
⊢ BddAbove (Set.range fun i ↦ (partialSups f) i)

Tactic:
· rwa [bddAbove_range_partialSups]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addLeftEmbedding c) (Ioc a b) = Ioc (c + a) (c + b)

Tactic:
rw [← coe_inj, coe_map, coe_Ioc, coe_Ioc]

Goal state after:
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addLeftEmbedding c) '' Set.Ioc a b = Set.Ioc (c + a) (c + b)
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addRightEmbedding c) (Ioc a b) = Ioc (a + c) (b + c)

Tactic:
rw [← coe_inj, coe_map, coe_Ioc, coe_Ioc]

Goal state after:
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addRightEmbedding c) '' Set.Ioc a b = Set.Ioc (a + c) (b + c)
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case succ
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
hf : Monotone f
m✝ n : ι
this : SuccOrder ι := LinearLocallyFiniteOrder.succOrder ι
m : ι
hm : n ≤ m
ih : (Ioc n m).sup (disjointed f) = f m \ f n
⊢ (Ioc n (succ m)).sup (disjointed f) = f (succ m) \ f n

Tactic:
by_cases h'm : IsMax m

Goal state after:
case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
hf : Monotone f
m✝ n : ι
this : SuccOrder ι := LinearLocallyFiniteOrder.succOrder ι
m : ι
hm : n ≤ m
ih : (Ioc n m).sup (disjointed f) = f m \ f n
h'm : IsMax m
⊢ (Ioc n (succ m)).sup (disjointed f) = f (succ m) \ f n

case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
hf : Monotone f
m✝ n : ι
this : SuccOrder ι := LinearLocallyFiniteOrder.succOrder ι
m : ι
hm : n ≤ m
ih : (Ioc n m).sup (disjointed f) = f m \ f n
h'm : ¬IsMax m
⊢ (Ioc n (succ m)).sup (disjointed f) = f (succ m) \ f n
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : IsIdempotentElem (q - p)
h : p * (q - p) + (q - p) * p = 0
hpq : Commute p q
⊢ p * q = p ∧ q * p = p

Tactic:
rw [hpq.eq, and_self, ← nsmul_right_inj (by simp : 2 ≠ 0), ← zero_add (2 • p)]

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : IsIdempotentElem (q - p)
h : p * (q - p) + (q - p) * p = 0
hpq : Commute p q
⊢ 2 • (q * p) = 0 + 2 • p
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
left✝ : 1 ∉ I
oJ : 1 ∈ J
a b : α
h : b ∈ Submodule.span α ↑I
oe : 1 = a • x + b
F : y * 1 = y * (a • x + b)
⊢ y * 1 ∈ I

Tactic:
F,

Goal state after:
α : Type u
inst✝ : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
left✝ : 1 ∉ I
oJ : 1 ∈ J
a b : α
h : b ∈ Submodule.span α ↑I
oe : 1 = a • x + b
F : y * 1 = y * (a • x + b)
⊢ y * (a • x + b) ∈ I
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case inl
n k : ℕ
h : n < k
⊢ ∑ m ∈ ∅, m.choose k = 0

Tactic:
sum_empty

Goal state after:
case inl
n k : ℕ
h : n < k
⊢ 0 = 0
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
c : R ⧸ I
m : (ι → R) ⧸ pi fun x ↦ I
c₁ : R
m₁ : ι → R
c₂ : R
m₂ : ι → R
⊢ (Submodule.quotientRel I) c₁ c₂ →
    (Submodule.quotientRel (pi fun x ↦ I)) m₁ m₂ → Submodule.Quotient.mk (c₁ • m₁) = Submodule.Quotient.mk (c₂ • m₂)

Tactic:
hc

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
c : R ⧸ I
m : (ι → R) ⧸ pi fun x ↦ I
c₁ : R
m₁ : ι → R
c₂ : R
m₂ : ι → R
hc : (Submodule.quotientRel I) c₁ c₂
⊢ (Submodule.quotientRel (pi fun x ↦ I)) m₁ m₂ → Submodule.Quotient.mk (c₁ • m₁) = Submodule.Quotient.mk (c₂ • m₂)
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ∑ a ∈ f.support, f a * ↑a = 1
this : (∑ i ∈ f.support, f i * ↑i) ^ (f.support.card * n + 1) ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
⊢ 1 ∈ span ((fun x ↦ x ^ (n + 1)) '' s)

Tactic:
rw [hf, one_pow] at this

Goal state after:
case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ∑ a ∈ f.support, f a * ↑a = 1
this : 1 ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
⊢ 1 ∈ span ((fun x ↦ x ^ (n + 1)) '' s)
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
⊢ (⨆ i, f i).NeBot ↔ ∃ i, (f i).NeBot

Tactic:
simp [neBot_iff]

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Subsingleton α
l : Filter α
inst✝ : l.NeBot
⊢ l = ⊤

Tactic:
by
  refine top_unique fun s hs => ?_
  obtain rfl : s = univ := Subsingleton.eq_univ_of_nonempty (nonempty_of_mem hs)
  exact univ_mem

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hm : Surjective m
⊢ comap m f = ⊥ ↔ f = ⊥

Tactic:
by
  rw [comap_eq_bot_iff_compl_range, hm.range_eq, compl_univ, empty_mem_iff_bot]

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
x : α
⊢ (l ⊔ pure x).HasBasis p fun i ↦ s i ∪ {x}

Tactic:
simp only [← principal_singleton, hl.sup_principal]

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ ∅ ∈ map m f → ∅ ∈ f

Tactic:
exact id

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p q : α → Prop
⊢ (∃ᶠ (x : α) in f, p x ∨ q x) ↔ (∃ᶠ (x : α) in f, p x) ∨ ∃ᶠ (x : α) in f, q x

Tactic:
by
  simp only [Filter.Frequently, ← not_and_or, not_or, eventually_and]

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ map f F ⊓ G ≤ map f (F ⊓ comap f G)

Tactic:
rintro U ⟨V, V_in, W, ⟨Z, Z_in, hZ⟩, h⟩
    apply mem_inf_of_inter (image_mem_map V_in) Z_in
    calc
      f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z) := by rw [image_inter_preimage]
      _ ⊆ f '' (V ∩ W) := by gcongr
      _ = f '' f ⁻¹' U := by rw [h]
      _ ⊆ U := image_preimage_subset f U

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ (map ?f (F ⊓ comap f G)).NeBot ↔ (map f F ⊓ G).NeBot

pp: case f
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ α → ?m.13

pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ Type ?u.26

Tactic:
Filter.push_pull

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ (map f F ⊓ G).NeBot ↔ (map f F ⊓ G).NeBot
Module: Mathlib.Algebra.Module.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : Semiring R
A : Type ?u.8
inst✝⁴ : Semiring A
inst✝³ : Module R A
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
inst✝ : Module A β
e : α ≃+ β
⊢ ∀ (b : α), 1 • b = b

Tactic:
by simp [Equiv.smul_def]

Goal state after:
Module: Mathlib.Algebra.Module.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : Semiring R
A : Type ?u.8
inst✝⁴ : Semiring A
inst✝³ : Module R A
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
inst✝ : Module A β
e : α ≃+ β
⊢ ∀ (a : A), a • 0 = 0

Tactic:
by simp [Equiv.smul_def]

Goal state after:
Module: Mathlib.Algebra.Module.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : Semiring R
A : Type ?u.8
inst✝⁴ : Semiring A
inst✝³ : Module R A
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
inst✝ : Module A β
e : α ≃+ β
⊢ ∀ (a : A) (x y : α), a • (x + y) = a • x + a • y

Tactic:
by simp [Equiv.smul_def]

Goal state after:
Module: Mathlib.Algebra.Module.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : Semiring R
A : Type ?u.8
inst✝⁴ : Semiring A
inst✝³ : Module R A
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
inst✝ : Module A β
e : α ≃+ β
⊢ ∀ (x : α), 0 • x = 0

Tactic:
by simp [Equiv.smul_def]

Goal state after:
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬M' < I) ↔ IsNoetherian R M

Tactic:
by
  rw [isNoetherian_iff, WellFounded.wellFounded_iff_has_min]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Injective ⇑f
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S ↑t = map f N
⊢ span S ↑t ≤ f.range

Tactic:
ht,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Injective ⇑f
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S ↑t = map f N
⊢ map f N ≤ f.range
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set (Set α)
h₁ : IsCofinal (⋃₀ s)
h₂ : #↑s < cof α
⊢ ∃ x ∈ s, IsCofinal x

Tactic:
contrapose! h₂
  simp_rw [not_isCofinal_iff] at h₂
  choose f hf using h₂
  refine (cof_le (s := range fun x ↦ f x.1 x.2) fun a ↦ ?_).trans mk_range_le
  obtain ⟨b, ⟨t, ht, hb⟩, hab⟩ := h₁ a
  simpa using ⟨t, ht, hab.trans (hf t ht b hb).le⟩

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
s : Finset A
hs : span R ↑s = ⊤
t : Finset M
ht : span A ↑t = ⊤
⊢ restrictScalars R (span A ↑t) = ⊤

Tactic:
ht,

Goal state after:
R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
s : Finset A
hs : span R ↑s = ⊤
t : Finset M
ht : span A ↑t = ⊤
⊢ restrictScalars R ⊤ = ⊤
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
ha : a ∉ s
⊢ f a ≤ b

Tactic:
have ha' := hs.isSuccLimit_of_notMem hs' ha

Goal state after:
case neg
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
ha : a ∉ s
ha' : IsSuccLimit a
⊢ f a ≤ b
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
ha : a ∉ s
ha' : IsSuccLimit a
c : α
⊢ c < a → f c ≤ b

Tactic:
hc

Goal state after:
case neg
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
ha : a ∉ s
ha' : IsSuccLimit a
c : α
hc : c < a
⊢ f c ≤ b
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mp
α : Type u
⊢ Small.{v, u} α → ∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'

Tactic:
rintro ⟨β, e⟩
    exact ⟨#β, lift_mk_eq.{u, _, v + 1}.2 e⟩

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
⊢ typeLT ↑s ≤ typeLT α

Tactic:
rw [type_le_iff']

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
⊢ Nonempty ((fun x1 x2 ↦ x1 < x2) ↪r fun x1 x2 ↦ x1 < x2)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s t : Set α
h : s ⊆ t
⊢ typeLT ↑s ≤ typeLT ↑t

Tactic:
rw [type_le_iff']

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s t : Set α
h : s ⊆ t
⊢ Nonempty ((fun x1 x2 ↦ x1 < x2) ↪r fun x1 x2 ↦ x1 < x2)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
x✝ : Ordinal.{?u.21}
⊢ x✝ * 0 = 0

Tactic:
by exact mul_eq_zero'.2 (.inr rfl)

Goal state after: