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

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
h_total_l : (Finsupp.linearCombination R v) l = v i
⊢ (Finsupp.linearCombination R v) l = (Finsupp.linearCombination R v) (Finsupp.single i 1)

Tactic:
h_total_l,

Goal state after:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
h_total_l : (Finsupp.linearCombination R v) l = v i
⊢ v i = (Finsupp.linearCombination R v) (Finsupp.single i 1)
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
h_total_l : (Finsupp.linearCombination R v) l = v i
h_total_eq : (Finsupp.linearCombination R v) l = (Finsupp.linearCombination R v) (Finsupp.single i 1)
l_eq : l = Finsupp.single i 1
⊢ ∃ a, f a = i

Tactic:
dsimp only [l] at l_eq

Goal state after:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
h_total_l : (Finsupp.linearCombination R v) l = v i
h_total_eq : (Finsupp.linearCombination R v) l = (Finsupp.linearCombination R v) (Finsupp.single i 1)
l_eq : Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩) = Finsupp.single i 1
⊢ ∃ a, f a = i
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
h_total_l : (Finsupp.linearCombination R v) l = v i
h_total_eq : (Finsupp.linearCombination R v) l = (Finsupp.linearCombination R v) (Finsupp.single i 1)
l_eq : Finsupp.embDomain f (repr ⟨v i, ⋯⟩) = Finsupp.single i 1
i' : ι'
hi' : repr ⟨v i, ⋯⟩ = Finsupp.single i' 1 ∧ f i' = i
⊢ ∃ a, f a = i

Tactic:
use i'

Goal state after:
case h
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⋯
l : ι →₀ R := ⋯
h_total_l : (Finsupp.linearCombination R v) l = v i
h_total_eq : (Finsupp.linearCombination R v) l = (Finsupp.linearCombination R v) (Finsupp.single i 1)
l_eq : Finsupp.embDomain f (repr ⟨v i, ⋯⟩) = Finsupp.single i 1
i' : ι'
hi' : repr ⟨v i, ⋯⟩ = Finsupp.single i' 1 ∧ f i' = i
⊢ f i' = i
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case succ
ι : Type u_1
M : Type u_2
m : ℕ
ih : ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i
n : Fin (m + 1) → ℕ
f : (i : Fin (m + 1)) → Fin (n i)
⊢ ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i

Tactic:
rw [Fin.prod_univ_castSucc, Fin.sum_univ_castSucc]

Goal state after:
case succ
ι : Type u_1
M : Type u_2
m : ℕ
ih : ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i
n : Fin (m + 1) → ℕ
f : (i : Fin (m + 1)) → Fin (n i)
⊢ ∑ i, ↑(f i.castSucc) * ∏ j, n (Fin.castLE ⋯ j) + ↑(f (Fin.last m)) * ∏ j, n (Fin.castLE ⋯ j) <
    (∏ i, n i.castSucc) * n (Fin.last m)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hn0 : 0 < n
⊢ 2 * (m * n / 2) = 2 * (m * (n / 2) + m / 2)

Tactic:
rw [mul_add, two_mul_odd_div_two hm1, mul_left_comm, two_mul_odd_div_two hn1,
      two_mul_odd_div_two (Nat.odd_mul_odd hm1 hn1), Nat.mul_sub, mul_one, ←
      Nat.add_sub_assoc (by lia), Nat.sub_add_cancel (Nat.le_mul_of_pos_right m hn0)]

Goal state after:
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ℤ
⊢ ↑↑x = (x % ↑n).toNat

Tactic:
by
  rw [Fin.intCast_def']
  split <;> rename_i h
  · simp [Int.emod_natAbs_of_nonneg h]
  · simp only [Fin.val_neg, Fin.natCast_eq_zero, Fin.val_natCast]
    split <;> rename_i h
    · rw [← Int.natCast_dvd] at h
      rw [Int.emod_eq_zero_of_dvd h, Int.toNat_zero]
    · rw [Int.emod_natAbs_of_neg (by lia) (NeZero.ne n),
        if_neg (by rwa [← Int.natCast_dvd] at h)]
      have : x % n < n := Int.emod_lt_of_pos x (by have := NeZero.ne n; lia)
      lia

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
this : Fintype α
⊢ ∏ a, Nat.card β = Nat.card β ^ Nat.card α

Tactic:
Finset.prod_const,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Finite α
this : Fintype α
⊢ Nat.card β ^ Finset.univ.card = Nat.card β ^ Nat.card α
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 : IsEmpty β
⊢ card (α → β) = 0 ^ ⊤

Tactic:
zero_epow_top,

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
x✝ : ∃ s, s.card = n ∧ LinearIndepOn R id ↑s
s : Finset M
card_s : s.card = n
ind_s : LinearIndepOn R id ↑s
⊢ #↑↑s = ↑n

Tactic:
simpa using card_s

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

Goal state before:
pp: α : Type u_1
e : α
⊢ {e}.encard = 1

Tactic:
by
  rw [encard, ENat.card_eq_coe_fintype_card, card_singleton, Nat.cast_eq_one]

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

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = ↑n
hk : ↑n + 1 ≤ s.encard
hne : t₀ ≠ s
x : α
hx : x ∈ s ∧ x ∉ t₀
⊢ (insert x t₀).encard = ↑n + 1

Tactic:
encard_insert_of_notMem hx.2,

Goal state after:
α : Type u_1
s : Set α
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = ↑n
hk : ↑n + 1 ≤ s.encard
hne : t₀ ≠ s
x : α
hx : x ∈ s ∧ x ∉ t₀
⊢ t₀.encard + 1 = ↑n + 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
h : (f '' s).encard = s.encard
hne : Nonempty α
⊢ InjOn f s

Tactic:
rw [← (f.invFunOn_injOn_image s).encard_image] at h

Goal state after:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
hne : Nonempty α
h : (Function.invFunOn f s '' f '' s).encard = s.encard
⊢ InjOn f s
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : 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
n : ℕ
N✝ : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N✝), LinearIndependent R (Subtype.val ∘ v) → m ≤ n
this : DecidableEq M
N : Submodule R M
a✝ : N ≤ ⊥
x : M
⊢ x ∈ ⊥ → (∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0) → P N

Tactic:
x_mem

Goal state after:
ι : 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
n : ℕ
N✝ : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N✝), LinearIndependent R (Subtype.val ∘ v) → m ≤ n
this : DecidableEq M
N : Submodule R M
a✝ : N ≤ ⊥
x : M
x_mem : x ∈ ⊥
⊢ (∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0) → P N
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Infinite β
this : Infinite α
⊢ Nat.card α = 0

Tactic:
exact Nat.card_eq_zero_of_infinite

Goal state after:
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 ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N'

Tactic:
x_mem

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
⊢ (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N'
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
hx : x ∈ s
h : ¬x = a
⊢ f₀ x ∈ t

Tactic:
· exact (hf₀s x hx h).1

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
y : A
⊢ Commute z (∑ a ∈ (b.repr y).support, (b.repr y) a • b a)

Tactic:
commute_iff_eq,

Goal state after:
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
y : A
⊢ z * ∑ a ∈ (b.repr y).support, (b.repr y) a • b a = (∑ a ∈ (b.repr y).support, (b.repr y) a • b a) * z
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊂ t
this✝ : Fintype ↑t
this : Fintype ↑s
⊢ Nat.card ↑s < Nat.card ↑t

Tactic:
simp only [Nat.card_eq_fintype_card]

Goal state after:
α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊂ t
this✝ : Fintype ↑t
this : Fintype ↑s
⊢ Fintype.card ↑s < Fintype.card ↑t
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.ncard = 2 ↔ s.encard = 2

Tactic:
ncard_def

Goal state after:
α : Type u_1
s : Set α
⊢ s.encard.toNat = 2 ↔ s.encard = 2
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.ncard = 3 ↔ s.encard = 3

Tactic:
ncard_def

Goal state after:
α : Type u_1
s : Set α
⊢ s.encard.toNat = 3 ↔ s.encard = 3
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.ncard = 4 ↔ s.encard = 4

Tactic:
ncard_def

Goal state after:
α : Type u_1
s : Set α
⊢ s.encard.toNat = 4 ↔ s.encard = 4
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrderTop α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a : α
⊢ Ioi (a - 1) = Ici a

Tactic:
by
  simpa [pred_eq_sub_one] using Ioi_pred_eq_Ici a

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

Goal state before:
pp: α : Type u_2
r : α → α → Prop
inst✝¹ : IsTrans α r
γ : Type u_3
inst✝ : Nonempty γ
f : γ → α
D : Directed r f
s : Set γ
hs : s.Finite
⊢ ∃ z, ∀ i ∈ s, r (f i) (f z)

Tactic:
convert! D.finset_le hs.toFinset using 3; rw [Set.Finite.mem_toFinset]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x ↦ x + d) (Ioi a ∩ Iic b) (Ioc (a + d) (b + d))

Tactic:
← Ioi_inter_Iic

Goal state after:
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x ↦ x + d) (Ioi a ∩ Iic b) (Ioi (a + d) ∩ Iic (b + d))
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: n : ℕ
⊢ n ! * n.succ = (n + 1) * n !

Tactic:
Nat.succ_eq_add_one,

Goal state after:
n : ℕ
⊢ n ! * (n + 1) = (n + 1) * n !
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: n : ℕ
⊢ ∑ i ∈ range n, i = n * (n - 1) / 2

Tactic:
rw [← sum_range_id_mul_two n, Nat.mul_div_cancel _ Nat.zero_lt_two]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
⊢ ∃ p, p.IsPrime ∧ I ≤ p ∧ Disjoint ↑p ↑S

Tactic:
have ⟨p, hIp, hp⟩ := zorn_le_nonempty₀ {p : Ideal α | Disjoint (p : Set α) S}
    (fun c hc hc' x hx ↦ ?_) I disjoint
  · exact ⟨p, isPrime_of_maximally_disjoint _ _ hp.1 (fun _ ↦ hp.not_prop_of_gt), hIp, hp.1⟩
  cases isEmpty_or_nonempty c
  · exact ⟨I, disjoint, fun J hJ ↦ isEmptyElim (⟨J, hJ⟩ : c)⟩
  refine ⟨sSup c, Set.disjoint_left.mpr fun x hx ↦ ?_, fun _ ↦ le_sSup⟩
  have ⟨p, hp⟩ := (Submodule.mem_iSup_of_directed _ hc'.directed).mp (sSup_eq_iSup' c ▸ hx)
  exact Set.disjoint_left.mp (hc p.2) hp

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case inr.h
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
⊢ x = y

Tactic:
rw [← x.single_add_erase 0, ← y.single_add_erase 0]

Goal state after:
case inr.h
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
⊢ Finsupp.single 0 (x 0) + erase 0 x = Finsupp.single 0 (y 0) + erase 0 y
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: case a
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
⊢ l ≤ l'

Tactic:
hl.le_basis_iff hl'

Goal state after:
case a
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
⊢ ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ map m (comap m f) = f ⊓ 𝓟 (range m)

Tactic:
by
  refine le_antisymm (le_inf map_comap_le <| le_principal_iff.2 range_mem_map) ?_
  rintro t' ⟨t, ht, sub⟩
  refine mem_inf_principal.2 (mem_of_superset ht ?_)
  rintro _ hxt ⟨x, rfl⟩
  exact sub hxt

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

Goal state before:
pp: α : Type u
s t : Set α
⊢ 𝓟 s ⊓ 𝓟 t ≤ 𝓟 (s ∩ t)

Tactic:
simp only [le_principal_iff, mem_inf_iff]

Goal state after:
α : Type u
s t : Set α
⊢ ∃ t₁ ∈ 𝓟 s, ∃ t₂ ∈ 𝓟 t, s ∩ t = t₁ ∩ t₂
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : Filter β
hα : IsEmpty α
⊢ (comap Prod.snd f).NeBot ↔ Nonempty α ∧ f.NeBot

Tactic:
rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]; simp

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:
map_eq_bot_iff

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ f = ⊥ ↔ f = ⊥
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
F : Filter α
s : Set α
⊢ map Subtype.val (comap Subtype.val F) = ⊥ ↔ comap Subtype.val F = ⊥

Tactic:
map_eq_bot_iff

Goal state after:
α : Type u_1
F : Filter α
s : Set α
⊢ comap Subtype.val F = ⊥ ↔ comap Subtype.val F = ⊥
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : IsCofinal s
x : α
⊢ ∃ i ∈ s, x ∈ Iio i

Tactic:
obtain ⟨y, hy⟩ := exists_gt x

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : IsCofinal s
x y : α
hy : x < y
⊢ ∃ i ∈ s, x ∈ Iio i
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : (N : Submodule R M) → N.FG → Prop
bot : motive ⊥ ⋯
sup : ∀ (N : Submodule R M) (x : M) (hN : N.FG), motive N hN → motive (N ⊔ R ∙ x) ⋯
N : Submodule R M
hN : N.FG
⊢ motive N hN

Tactic:
classical
  obtain ⟨s, rfl⟩ := hN
  induction s using Finset.induction with
  | empty => simp [bot]
  | insert x s hxs ih => simpa [span_insert, sup_comm] using sup (span R s) x (by use s) ih

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

Goal state before:
pp: case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
⊢ f i < iSup f

Tactic:
by_contra! hle

Goal state after:
case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : iSup f ≤ f i
⊢ False
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
H₁ : b ^ (log.go y b y).snd ≤ y
H₂ : y < b ^ ((log.go y b y).snd + 1)
⊢ log b y < x ↔ y < b ^ x

Tactic:
rw [log, if_neg (Nat.not_le_of_lt hb)]

Goal state after:
b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
H₁ : b ^ (log.go y b y).snd ≤ y
H₂ : y < b ^ ((log.go y b y).snd + 1)
⊢ (log.go y b y).snd < x ↔ y < b ^ x
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_1
β : Type u_2
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
a : Ordinal.{max u v}
ha : a < o'
⊢ g a ha < o

Tactic:
rw [← hg]

Goal state after:
α : Type u_1
β : Type u_2
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
a : Ordinal.{max u v}
ha : a < o'
⊢ g a ha < o'.blsub g
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : IsSuccLimit o
⊢ ∀ a < o, f a < f (succ a)

Tactic:
exact fun a _ => H.strictMono (lt_succ a)

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

Goal state before:
pp: case limit
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal.{u_1}
l : IsSuccLimit b
a✝ : ∀ o' < b, 0 < a ^ o'
⊢ 0 < a ^ b

Tactic:
| limit b l _ =>

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

Goal state before:
pp: case refine_1.inl.inl
b : Ordinal.{u_1}
⊢ 0 ^ b ≤ 1

pp: case refine_1.inl.inr
b : Ordinal.{u_1}
⊢ 1 ^ b ≤ 1

pp: case refine_1.inr
a : Ordinal.{u_1}
⊢ a ^ 0 ≤ 1

Tactic:
· exact zero_opow_le b

Goal state after:
case refine_1.inl.inr
b : Ordinal.{u_1}
⊢ 1 ^ b ≤ 1

case refine_1.inr
a : Ordinal.{u_1}
⊢ a ^ 0 ≤ 1
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b : Ordinal.{u_1}
ha : 1 < a
hb : 1 < b
⊢ a < a ^ b

Tactic:
by
  conv_lhs => rw [← opow_one a]
  rwa [opow_lt_opow_iff_right ha]

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

Goal state before:
pp: case inr.inl.inr
o : Ordinal.{u_1}
ho : o ≠ 0
hbo : o < 1
hb : 1 ≤ 1
⊢ log 1 o = 0

Tactic:
exact log_one_left o

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

Goal state before:
pp: b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ log b (b ^ x) = x

Tactic:
by
  convert! log_opow_mul hb x zero_ne_one.symm using 1
  · rw [mul_one]
  · rw [log_one_right, add_zero]

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

Goal state before:
pp: case inl
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ b ^ log b x * b ^ log b y ≤ x * y

Tactic:
exact mul_le_mul' (opow_log_le_self b hx) (opow_log_le_self b hy)

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

Goal state before:
pp: case pos.inr
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
hs' : s.Nonempty
⊢ IsPrincipal op (sSup s)

Tactic:
simp only [IsPrincipal, lt_csSup_iff hs hs', forall_exists_index, and_imp]

Goal state after:
case pos.inr
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
hs' : s.Nonempty
⊢ ∀ ⦃a b : Ordinal.{u_1}⦄, ∀ x ∈ s, a < x → ∀ x ∈ s, b < x → ∃ b_1 ∈ s, op a b < b_1
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case mpr.refine_1
a✝ b : Ordinal.{u_1}
hb : b ≠ 0
a : Ordinal.{u_1}
ha : a < b
n : ℕ
hn : a✝ < ω ^ (ω ^ a * ↑n)
⊢ ω ^ a * ↑n < ω ^ a * ↑(n + 1)

pp: case mpr.refine_2
a✝ b : Ordinal.{u_1}
hb : b ≠ 0
a : Ordinal.{u_1}
ha : a < b
n : ℕ
hn : a✝ < ω ^ (ω ^ a * ↑n)
⊢ a✝ < ω ^ (ω ^ a * ↑n) * ↑1

Tactic:
· simp [mul_lt_mul_iff_right₀, opow_pos]

Goal state after:
case mpr.refine_2
a✝ b : Ordinal.{u_1}
hb : b ≠ 0
a : Ordinal.{u_1}
ha : a < b
n : ℕ
hn : a✝ < ω ^ (ω ^ a * ↑n)
⊢ a✝ < ω ^ (ω ^ a * ↑n) * ↑1