mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: case inr.inr.inr.inl.a
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
b_1 : card β = 1
⊢ card (α → β) ≤ 1

Tactic:
let := (card_le_one_iff_subsingleton β).1 b_1.le

Goal state after:
case inr.inr.inr.inl.a
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
b_1 : card β = 1
this : Subsingleton β := (card_le_one_iff_subsingleton β).mp (Eq.le b_1)
⊢ card (α → β) ≤ 1
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: case h₁
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
⊢ ∀ (i : { s // LinearIndepOn R id s }), #↑↑i ≤ 1

Tactic:
have := Module.subsingleton R M
    simp [Set.subsingleton_of_subsingleton]

Goal state after:
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
h : Module.rank R M ≠ 0
⊢ ?m.16

Tactic:
by rwa [← Cardinal.one_le_iff_ne_zero, one_le_rank_iff] at h

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

Goal state before:
pp: R : Type u
M : Type v
N : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Injective ⇑f
⊢ finrank R ↥f.range = finrank R M

Tactic:
(LinearEquiv.ofInjective f hf).finrank_eq

Goal state after:
R : Type u
M : Type v
N : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Injective ⇑f
⊢ finrank R ↥f.range = finrank R ↥f.range
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ (xgcd 0 s).fst = 0

Tactic:
xgcd,

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ (xgcdAux 0 1 0 s 0 1).snd.fst = 0
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ (xgcdAux 0 1 0 s 0 1).snd.fst = 0

Tactic:
xgcd_zero_left

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ (s, 0, 1).snd.fst = 0
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ (xgcd 0 s).snd = 1

Tactic:
xgcd,

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ (xgcdAux 0 1 0 s 0 1).snd.snd = 1
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ (xgcdAux 0 1 0 s 0 1).snd.snd = 1

Tactic:
xgcd_zero_left

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ (s, 0, 1).snd.snd = 1
Module: Mathlib.Algebra.EuclideanDomain.Int

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
⊢ ↑(a % b).natAbs < ↑b.natAbs

Tactic:
rw [Int.natAbs_of_nonneg (Int.emod_nonneg _ b0), ← Int.abs_eq_natAbs]

Goal state after:
a b : ℤ
b0 : b ≠ 0
⊢ a % b < |b|
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ (insert a (s \ {b})).encard = s.encard

Tactic:
rw [encard_insert_of_notMem, encard_sdiff_singleton_add_one hb]
  simp_all only [mem_sdiff, mem_singleton_iff, false_and, not_false_eq_true]

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

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

Tactic:
obtain ⟨k, rfl⟩ := exists_add_of_le hsk

Goal state after:
case inr
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : s.encard + k ≤ t.encard
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + k
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
⊢ P N

Tactic:
by
  haveI : DecidableEq M := Classical.decEq M
  have Pbot : P ⊥ := by
    apply ih
    intro N _ x x_mem x_ortho
    exfalso
    rw [mem_bot] at x_mem
    simpa [x_mem] using x_ortho 1 0 N.zero_mem
  induction n generalizing N with
  | zero =>
    suffices N = ⊥ by rwa [this]
    apply Basis.eq_bot_of_rank_eq_zero b _ fun m hv => Nat.le_zero.mp (rank_le _ hv)
  | succ n rank_ih =>
    apply ih
    intro N' N'_le x x_mem x_ortho
    apply rank_ih
    intro m v hli
    refine Nat.succ_le_succ_iff.mp (rank_le (Fin.cons ⟨x, x_mem⟩ fun i => ⟨v i, N'_le (v i).2⟩) ?_)
    convert! hli.finCons' x _ ?_
    · ext i
      refine Fin.cases ?_ ?_ i <;> simp
    · intro c y hy hc
      refine x_ortho c y (Submodule.span_le.mpr ?_ hy) hc
      rintro _ ⟨z, rfl⟩
      exact (v z).2

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)
c d : A
⊢ z * ((linearCombination R ⇑b) (b.repr c) * d) = z * (linearCombination R ⇑b) (b.repr c) * d

Tactic:
← b.linearCombination_repr d,

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)
c d : A
⊢ z * ((linearCombination R ⇑b) (b.repr c) * (linearCombination R ⇑b) (b.repr d)) =
    z * (linearCombination R ⇑b) (b.repr c) * (linearCombination R ⇑b) (b.repr d)
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)
c d : A
⊢ (linearCombination R ⇑b) (b.repr c) * d * z = (linearCombination R ⇑b) (b.repr c) * (d * z)

Tactic:
← b.linearCombination_repr d,

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)
c d : A
⊢ (linearCombination R ⇑b) (b.repr c) * (linearCombination R ⇑b) (b.repr d) * z =
    (linearCombination R ⇑b) (b.repr c) * ((linearCombination R ⇑b) (b.repr d) * z)
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : IsTorsionFree R S
b : Basis ι S M
m : M
h✝ : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
i : ι
x✝ : i ∈ (b.repr m).support
w✝ : R
h : (algebraMap R S) w✝ = (b.repr m) i
⊢ (algebraMap R S) w✝ • b i ∈ span R (range ⇑b)

Tactic:
algebraMap_smul

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : IsTorsionFree R S
b : Basis ι S M
m : M
h✝ : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
i : ι
x✝ : i ∈ (b.repr m).support
w✝ : R
h : (algebraMap R S) w✝ = (b.repr m) i
⊢ w✝ • b i ∈ span R (range ⇑b)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case convert_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
⊢ ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s.toFinset) (ha₂ : a₂ ∈ s.toFinset), f'' a₁ ha₁ = f'' a₂ ha₂ → a₁ = a₂

pp: case convert_3
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
⊢ t.toFinset.card ≤ s.toFinset.card

Tactic:
· intro a₁ a₂ ha₁ ha₂ h
    rw [mem_toFinset] at ha₁ ha₂
    exact hinj _ _ ha₁ ha₂ h

Goal state after:
case convert_3
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
⊢ t.toFinset.card ≤ s.toFinset.card
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
x : α ⧸ ⊥
⊢ ↑(Quotient.lift id ⋯ x) = x

Tactic:
induction x using Quotient.inductionOn; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : Finite ↑s
f : α → β
⊢ s.ncard ≤ (f '' s).ncard + 1 ↔
    ∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, ∀ d ∈ s, f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}

Tactic:
by
  simpa [Subtype.ext_iff, ← (Set.image_injective.mpr Subtype.val_injective).eq_iff,
     Set.image_insert_eq, Set.image_singleton] using
      (Set.surjective_mapsTo_image_restrict f s).card_le_card_add_one_iff

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✝ : IsDirectedOrder α
f : ι → α
⊢ BddAbove (Set.range f)

Tactic:
by
  obtain ⟨M, hM⟩ := Finite.exists_le f
  refine ⟨M, fun a ha => ?_⟩
  obtain ⟨b, rfl⟩ := ha
  exact hM b

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ toZ i0 i ≤ 0

Tactic:
rw [toZ_of_lt hi]
    lia

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : m = n + 1
⊢ toZ i0 (pred^[n + 1] i0) = -↑(n + 1)

pp: case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : ¬m = n + 1
⊢ toZ i0 (pred^[n + 1] i0) = -↑(n + 1)

Tactic:
· nth_rw 2 [← hmn]
    rw [Int.toNat_eq_max, toZ_of_lt this, max_eq_left, neg_neg]
    rw [neg_neg]
    exact Int.natCast_nonneg _

Goal state after:
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : ¬m = n + 1
⊢ toZ i0 (pred^[n + 1] i0) = -↑(n + 1)
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ ∏ i ∈ Icc a b, f i = ∏ i ∈ Icc ↑a ↑b, if h : i < n then f ⟨i, h⟩ else 1

Tactic:
rw [← prod_ite_mem_eq, prod_fin_eq_prod_range]
  apply prod_congr_of_eq_on_inter <;> grind

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: case refine_2
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ n - k + (l + j) = n

Tactic:
hl

Goal state after:
case refine_2
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ n - k + k = n
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: case refine_2
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ l + j + k = n

Tactic:
hl

Goal state after:
case refine_2
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ n - k + k = n
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ (1 - a) * 1 - (1 - a) * a = 1 - a

Tactic:
mul_one,

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ 1 - a - (1 - a) * a = 1 - a
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ a * 1 - a * a = 0

Tactic:
mul_one,

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ a - a * a = 0
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : R
⊢ IsIdempotentElem a ↔ a * 1 - a * a = 0

Tactic:
mul_one,

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
a : R
⊢ IsIdempotentElem a ↔ a - a * a = 0
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ 1 = 1 * 1 * 1

Tactic:
mul_one,

Goal state after:
case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ 1 = 1 * 1
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
ι : Type u_1
x : ι → α
⊢ span (range x) = ⨆ i, span {x i}

Tactic:
rw [← span_iUnion, iUnion_singleton_eq_range]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
⊢ (x + y) ^ n = ∑ m ∈ antidiagonal n, n.choose m.1 • (x ^ m.1 * y ^ m.2)

Tactic:
by
  simp_rw [Nat.sum_antidiagonal_eq_sum_range_succ fun m p ↦ n.choose m • (x ^ m * y ^ p),
    nsmul_eq_mul, cast_comm, h.add_pow]

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

Goal state before:
pp: α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
b₁ b₂ : α
h₁ : b₁ ≠ 0
h₂ : ¬IsUnit b₂
h : span {b₁} ≤ span {b₁ * b₂}
⊢ b₁ * b₂ ∣ b₁ * 1

Tactic:
mul_one,

Goal state after:
α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
b₁ b₂ : α
h₁ : b₁ ≠ 0
h₂ : ¬IsUnit b₂
h : span {b₁} ≤ span {b₁ * b₂}
⊢ b₁ * b₂ ∣ b₁
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
h : x ∈ (LinearMap.toSpanSingleton R R e).ker
⊢ x * 1 - 0 = x

Tactic:
mul_one,

Goal state after:
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
h : x ∈ (LinearMap.toSpanSingleton R R e).ker
⊢ x - 0 = x
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
h : ¬n = 0
⊢ ∑ i ∈ range (n + 1), n * n.choose i = n * 2 ^ n

Tactic:
by
      rw [← mul_sum, Nat.sum_range_choose]

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

Goal state before:
pp: case isUnit_or_isUnit.refine_1
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
c d : α
ha : a = a * c * (a * d)
huv : ¬IsUnit (a * c) ∧ ¬IsUnit (a * d)
⊢ span {a} = span {a * (c * d)}

Tactic:
apply le_antisymm <;> rw [span_singleton_le_span_singleton]

Goal state after:
case isUnit_or_isUnit.refine_1.a
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
c d : α
ha : a = a * c * (a * d)
huv : ¬IsUnit (a * c) ∧ ¬IsUnit (a * d)
⊢ a * (c * d) ∣ a

case a
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
c d : α
ha : a = a * c * (a * d)
huv : ¬IsUnit (a * c) ∧ ¬IsUnit (a * d)
⊢ a ∣ a * (c * d)
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ℕ
⊢ span ((fun x ↦ x ^ n) '' s) = ⊤

Tactic:
rw [eq_top_iff_one]

Goal state after:
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ℕ
⊢ 1 ∈ span ((fun x ↦ x ^ n) '' s)
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → s' i' ∈ l
t : Set α
ht✝ : t ∈ l
i : ι
hi : p i
ht : s i ⊆ t
i' : ι'
hi' : p' i'
hs's : s' i' ⊆ s i
⊢ ∃ i, p' i ∧ s' i ⊆ t

Tactic:
exact ⟨i', hi', hs's.trans ht⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
l : Filter β
s : Set α
⊢ sᶜ ∈ comap f l ↔ (f '' s)ᶜ ∈ l

Tactic:
rw [mem_comap_iff_compl, compl_compl]

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

Goal state before:
pp: α : 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'
⊢ ∀ (t : Set α), t ∈ l ⊓ l' ↔ ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t

Tactic:
by
    intro t
    constructor
    · simp only [mem_inf_iff, hl.mem_iff, hl'.mem_iff]
      rintro ⟨t, ⟨i, hi, ht⟩, t', ⟨i', hi', ht'⟩, rfl⟩
      exact ⟨⟨i, i'⟩, ⟨hi, hi'⟩, inter_subset_inter ht ht'⟩
    · rintro ⟨⟨i, i'⟩, ⟨hi, hi'⟩, H⟩
      exact mem_inf_of_inter (hl.mem_of_mem hi) (hl'.mem_of_mem hi') H

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

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
B : ∀ (s t : Set α), q s → q t → q (s ∩ t)
C : ∀ (i : ι), ∀ s ∈ f i, q s
⊢ univ ∈ {t | q t}

Tactic:
simpa [q] using uni

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

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

Tactic:
filter_eq_bot_of_isEmpty (f.comap _),

Goal state after:
case inl
α : Type u_1
β : Type u_2
f : Filter α
h✝ : IsEmpty β
⊢ ⊥.NeBot ↔ f.NeBot ∧ Nonempty β
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:
filter_eq_bot_of_isEmpty (f.comap _),

Goal state after:
case inl
α : Type u_1
β : Type u_2
f : Filter β
hα : IsEmpty α
⊢ ⊥.NeBot ↔ Nonempty α ∧ f.NeBot
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case inl
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : IsEmpty ((j : ι) → α j)
⊢ (comap (eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot

Tactic:
filter_eq_bot_of_isEmpty (f.comap _),

Goal state after:
case inl
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : IsEmpty ((j : ι) → α j)
⊢ ⊥.NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot
Module: Mathlib.Order.Filter.AtTopBot.Tendsto

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝¹ : Preorder ι
inst✝ : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
⊢ Tendsto u atTop atTop

Tactic:
apply h.tendsto_atTop_atTop
  intro b
  rcases not_bddAbove_iff.1 H b with ⟨_, ⟨N, rfl⟩, hN⟩
  exact ⟨N, le_of_lt hN⟩

Goal state after:
Module: Mathlib.Data.Set.Finite.Lemmas

Goal state before:
pp: α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
⊢ C S

Tactic:
have : Finite S := Finite.to_subtype h
  have : Finite {T : Set α // T ⊆ S} := Finite.of_equiv (Set S) (Equiv.Set.powerset S).symm
  rw [← Subtype.coe_mk (p := (· ⊆ S)) _ le_rfl]
  rw [← Subtype.coe_mk (p := (· ⊆ S)) _ hS0] at H0
  refine Finite.to_wellFoundedGT.wf.induction_bot' (fun s hs hs' ↦ ?_) H0
  obtain ⟨a, ⟨ha1, ha2⟩, ha'⟩ := H1 s (ssubset_of_ne_of_subset hs s.2) hs'
  exact ⟨⟨insert a s.1, insert_subset ha1 s.2⟩, Set.ssubset_insert ha2, ha'⟩

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

Goal state before:
pp: case mpr
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding

Tactic:
← lift_id (type s)

Goal state after:
case mpr
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
⊢ lift.{max (u + 1) v, max (u + 1) v} (type s) ∈ Set.range ⇑liftInitialSeg.toRelEmbedding
Module: Mathlib.SetTheory.Ordinal.Univ

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

Tactic:
rintro ⟨c, hc⟩

Goal state after:
case mpr
α : Type u
c : Cardinal.{v}
hc : lift.{v + 1, u} #α = lift.{max u (v + 1), v} c
⊢ Small.{v, u} α
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_1
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
ha : r a b
⊢ ∀ (a_1 : { x // r x a }), (PrincipalSeg.ofElement r a).toRelEmbedding a_1 ∈ fun x ↦ r x b

Tactic:
rintro ⟨c, hc⟩

Goal state after:
case refine_1
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
ha : r a b
c : α
hc : r c a
⊢ (PrincipalSeg.ofElement r a).toRelEmbedding ⟨c, hc⟩ ∈ fun x ↦ r x b
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_4
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ ∀ (α_1 : Type u) (r_1 : α_1 → α_1 → Prop) [inst : IsWellOrder α_1 r_1],
    type r_1 < type r → type r_1 ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯)

Tactic:
rintro β s wo ⟨g⟩

Goal state after:
case refine_4
α : Type u
β✝ : Type v
γ : Type w
r✝ : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
β : Type u
s : β → β → Prop
wo : IsWellOrder β s
g : s ≺i r
⊢ type s ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
hc : IsSuccLimit c
⊢ a < b + c ↔ ∃ d < c, a < b + d

Tactic:
by
  rw [lt_add_iff hc.ne_bot]
  constructor <;> rintro ⟨d, hd, ha⟩
  · refine ⟨_, hc.succ_lt hd, ?_⟩
    rwa [succ_eq_add_one, ← add_assoc, lt_add_one_iff]
  · exact ⟨d, hd, ha.le⟩

Goal state after: