mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
h : c ∣ b
⊢ a % b % c = a % c

Tactic:
nth_rw 2 [← div_add_mod a b]
  rcases h with ⟨d, rfl⟩
  rw [mul_assoc, mul_add_mod_self]

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

Goal state before:
pp: case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ n * (m / n) ≤ m

Tactic:
mul_comm

Goal state after:
case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ m / n * n ≤ m
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inr
b k n : ℕ
hk : k > 0
hb : 1 ≥ b
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k

Tactic:
suffices (k - 1) / k = 0 by grind [clog_of_left_le_one, Nat.pow_le_one_iff]
      apply Nat.div_eq_of_lt
      grind

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

Goal state before:
pp: case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
c : Ordinal.{u}
a : ↑(Set.Iio o)
⊢ f i (derivFamily f ↑a) ≤ c ↔ derivFamily f ↑a ≤ c

Tactic:
rw [IH _ a.2]

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:
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.Principal

Goal state before:
pp: a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : IsPrincipal op o
n : ℕ
⊢ (op a)^[n] a < o

Tactic:
by
  induction n with
  | zero => rwa [Function.iterate_zero]
  | succ n hn =>
    rw [Function.iterate_succ']
    exact ho hao hn

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

Goal state before:
pp: case a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ a ^ ω ≤ nfp (fun x ↦ a * x) b

Tactic:
rw [← nfp_mul_one ha]

Goal state after:
case a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x ↦ a * x) 1 ≤ nfp (fun x ↦ a * x) b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : ¬b = 0
⊢ a ^ ω ≤ b

Tactic:
rw [← nfp_mul_one ha]

Goal state after:
case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : ¬b = 0
⊢ nfp (fun x ↦ a * x) 1 ≤ b
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccLimit o
a : Ordinal.{u_1}
ha : ∀ b < o, preOmega b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ preOmega b < preOmega (succ b)

Tactic:
preOmega_lt_preOmega

Goal state after:
o : Ordinal.{u_1}
ho : IsSuccLimit o
a : Ordinal.{u_1}
ha : ∀ b < o, preOmega b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ b < succ b
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: x : Ordinal.{u_1}
| preOmega ω < preOmega x

Tactic:
preOmega_lt_preOmega

Goal state after:
x : Ordinal.{u_1}
| ω < x
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case type
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ Cardinal.lift.{v, u} (typeLT α).cof = (lift.{v, u} (typeLT α)).cof

Tactic:
| type α
   => 

Goal state after:
case type
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ Cardinal.lift.{v, u} (typeLT α).cof = (lift.{v, u} (typeLT α)).cof
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case type
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ (typeLT α).cof = 1 ↔ typeLT α ∈ range succ

Tactic:
| type α
   => 

Goal state after:
case type
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ (typeLT α).cof = 1 ↔ typeLT α ∈ range succ
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a b : Ordinal.{u_1}
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ (fun x1 x2 ↦ x1 * x2) ↑m ↑n < ω

Tactic:
dsimp only; rw [← natCast_mul]
    apply natCast_lt_omega0

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

Goal state before:
pp: a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a ≤ a * b

Tactic:
mul_comm

Goal state after:
a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a ≤ b * a
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_1.inr
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
ho₂ : 2 < o
⊢ o ≤ 2 ∨ o ∈ Set.range fun x ↦ ω ^ ω ^ x

Tactic:
· rcases isPrincipal_add_iff_zero_or_omega0_opow.1
        (isPrincipal_add_of_isPrincipal_mul ho ho₂.ne') with (rfl | ⟨a, rfl⟩)
      · exact (not_lt_zero ho₂).elim
      · rcases isPrincipal_add_iff_zero_or_omega0_opow.1
          (isPrincipal_add_of_isPrincipal_mul_opow one_lt_omega0 ho) with (rfl | ⟨b, rfl⟩)
        · simp
        · exact Or.inr ⟨b, rfl⟩

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

Goal state before:
pp: β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ #↑(⋃ j, ⋃ (_ : j < o), A j) ≤ c

Tactic:
simp_rw [← mem_Iio, biUnion_eq_iUnion, iUnion, iSup, ← ToType.mk.symm.surjective.range_comp]
  rw [← lift_le.{u}]
  apply ((mk_iUnion_le_lift _).trans _).trans_eq (mul_eq_self (aleph0_le_lift.2 hc))
  rw [mk_toType]
  refine mul_le_mul' ho (ciSup_le' ?_)
  intro i
  simpa using hA _ i.toOrd.prop

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

Goal state before:
pp: case inl
ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ i, f i) + c
bdd : BddAbove (range fun x ↦ f x + c)
hs : ⨆ i, f i < ℵ₀
⊢ (⨆ i, f i) + c ≤ ⨆ i, f i + c

Tactic:
obtain ⟨i, hi⟩ := exists_eq_ciSup_of_not_isSuccLimit hf (not_isSuccLimit_of_lt_aleph0 hs)
    exact hi ▸ le_ciSup bdd i

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

Goal state before:
pp: case pos.inl
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ i, f i) * c
bdd : BddAbove (range fun x ↦ f x * c)
hs : ⨆ i, f i < ℵ₀
⊢ (⨆ i, f i) * c ≤ ⨆ i, f i * c

Tactic:
obtain ⟨i, hi⟩ := exists_eq_ciSup_of_not_isSuccLimit hf (not_isSuccLimit_of_lt_aleph0 hs)
    exact hi ▸ le_ciSup bdd i

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

Tactic:
cases isEmpty_or_nonempty ι; · simp
  obtain rfl | h0 := eq_or_ne c 0; · simp
  by_cases hf : BddAbove (range f); swap
  · have hfc : ¬ BddAbove (range (f · * c)) := fun bdd ↦ hf
      ⟨⨆ i, f i * c, forall_mem_range.mpr fun i ↦ (le_mul_right h0).trans (le_ciSup bdd i)⟩
    simp [iSup, csSup_of_not_bddAbove, hf, hfc]
  have (i : ι) : f i * c ≤ (⨆ i, f i) * c := by grw [← le_ciSup hf i]
  refine le_antisymm ?_ (ciSup_le' this)
  have bdd : BddAbove (range (f · * c)) := ⟨_, forall_mem_range.mpr this⟩
  obtain hs | hs := lt_or_ge (⨆ i, f i) ℵ₀
  · obtain ⟨i, hi⟩ := exists_eq_ciSup_of_not_isSuccLimit hf (not_isSuccLimit_of_lt_aleph0 hs)
    exact hi ▸ le_ciSup bdd i
  rw [mul_eq_max_of_aleph0_le_left hs h0, max_le_iff]
  obtain ⟨i, hi⟩ := exists_lt_of_lt_ciSup' (one_lt_aleph0.trans_le hs)
  exact ⟨ciSup_mono bdd fun i ↦ le_mul_right h0,
    (le_mul_left (zero_lt_one.trans hi).ne').trans (le_ciSup bdd i)⟩

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
⊢ ⨆ i, f i * c = ⨆ i, c * f i

Tactic:
mul_comm

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hι : #ι = o.cof
⊢ ∃ f, o.cof.ord.blsub f = o

Tactic:
rcases Cardinal.exists_ord_eq ι with ⟨r, hr, hι'⟩

Goal state after:
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hι : #ι = o.cof
r : ι → ι → Prop
hr : IsWellOrder ι r
hι' : (#ι).ord = type r
⊢ ∃ f, o.cof.ord.blsub f = o
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = b
⊢ a ≤ #ι

Tactic:
rcases Cardinal.exists_ord_eq ι with ⟨r, hr, hι'⟩

Goal state after:
b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = b
r : ι → ι → Prop
hr : IsWellOrder ι r
hι' : (#ι).ord = type r
⊢ a ≤ #ι
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u_1}
h : ω ≤ o
⊢ (preAleph (o + 1)).ord.cof = preAleph (o + 1)

Tactic:
(isRegular_preAleph_add_one h).cof_ord

Goal state after:
o : Ordinal.{u_1}
h : ω ≤ o
⊢ preAleph (o + 1) = preAleph (o + 1)
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
hα : #α < ℵ₀
⊢ #α < ℵ_ 1

Tactic:
exact hα.trans aleph0_lt_aleph_one

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

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = #(α → β')
⊢ lift.{max u v, u} #(α ≃ α) = lift.{max u v, u} #(α → α)

Tactic:
lift_inj,

Goal state after:
α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = #(α → β')
⊢ #(α ≃ α) = #(α → α)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
inst✝ : Infinite α
H1 : ℵ₀ ≤ #α
⊢ (sum fun x ↦ #α) = #α

Tactic:
simp [H1]

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C✝ : ((i : ι) → Quotient (S i)) → Prop
f : ∀ (a : (i : ι) → α i), C✝ fun x ↦ ⟦a x⟧
q : (i : ι) → Quotient (S i)
m : Multiset ι
C : ((i : ι) → i ∈ m → Quotient (S i)) → Prop
⊢ (∀ (a : (i : ι) → i ∈ m → α i), C fun x1 x2 ↦ ⟦a x1 x2⟧) → ∀ (q : (i : ι) → i ∈ m → Quotient (S i)), C q

Tactic:
induction m using Quotient.ind

Goal state after:
case a
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C✝ : ((i : ι) → Quotient (S i)) → Prop
f : ∀ (a : (i : ι) → α i), C✝ fun x ↦ ⟦a x⟧
q : (i : ι) → Quotient (S i)
a✝ : List ι
C : ((i : ι) → i ∈ ⟦a✝⟧ → Quotient (S i)) → Prop
⊢ (∀ (a : (i : ι) → i ∈ ⟦a✝⟧ → α i), C fun x1 x2 ↦ ⟦a x1 x2⟧) → ∀ (q : (i : ι) → i ∈ ⟦a✝⟧ → Quotient (S i)), C q
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (Subtype.instSetoid_mathlib fun l ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun l ↦ ∀ (i : ι), i ∈ l) (fun s ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯)
    ⟨Finset.univ.val, ⋯⟩
a✝¹ b✝ : { l // ∀ (i : ι), i ∈ l }
a✝ : a✝¹ ≈ b✝
⊢ Quotient.map (fun a i ↦ a i ⋯) ⋯ (listChoice fun i x ↦ q i) =
    Quotient.map (fun a i ↦ a i ⋯) ⋯ (listChoice fun i x ↦ q i)

Tactic:
refine ind_fintype_pi (fun a ↦ ?_) q

Goal state after:
case refine_2
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (Subtype.instSetoid_mathlib fun l ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun l ↦ ∀ (i : ι), i ∈ l) (fun s ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯)
    ⟨Finset.univ.val, ⋯⟩
a✝¹ b✝ : { l // ∀ (i : ι), i ∈ l }
a✝ : a✝¹ ≈ b✝
a : (i : ι) → α i
⊢ Quotient.map (fun a i ↦ a i ⋯) ⋯ (listChoice fun i x ↦ (fun x ↦ ⟦a x⟧) i) =
    Quotient.map (fun a i ↦ a i ⋯) ⋯ (listChoice fun i x ↦ (fun x ↦ ⟦a x⟧) i)
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : Dual R R
r : R
⊢ f 1 * r = r * f 1

Tactic:
mul_comm

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : Dual R R
r : R
⊢ r * f 1 = r * f 1
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
W : Submodule R M
f : N →ₗ[R] M
⊢ map f.dualMap W.dualAnnihilator ≤ (comap f W).dualAnnihilator

Tactic:
intro

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
W : Submodule R M
f : N →ₗ[R] M
x✝ : Dual R N
⊢ x✝ ∈ map f.dualMap W.dualAnnihilator → x✝ ∈ (comap f W).dualAnnihilator
Module: Mathlib.Algebra.Algebra.Pi

Goal state before:
pp: α : Type u_1
β : Type u_2
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
A₃ : ι → Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → Semiring (A₁ i)
inst✝⁶ : (i : ι) → Semiring (A₂ i)
inst✝⁵ : (i : ι) → Semiring (A₃ i)
inst✝⁴ : (i : ι) → Algebra R (A₁ i)
inst✝³ : (i : ι) → Algebra R (A₂ i)
inst✝² : (i : ι) → Algebra R (A₃ i)
S : Type u_8
inst✝¹ : Semiring S
inst✝ : Algebra R S
⊢ ∀ (x : R),
    (RingEquiv.sumArrowEquivProdArrow α β S) ((algebraMap R (α ⊕ β → S)) x) = (algebraMap R ((α → S) × (β → S))) x

Tactic:
intro

Goal state after:
α : Type u_1
β : Type u_2
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
A₃ : ι → Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → Semiring (A₁ i)
inst✝⁶ : (i : ι) → Semiring (A₂ i)
inst✝⁵ : (i : ι) → Semiring (A₃ i)
inst✝⁴ : (i : ι) → Algebra R (A₁ i)
inst✝³ : (i : ι) → Algebra R (A₂ i)
inst✝² : (i : ι) → Algebra R (A₃ i)
S : Type u_8
inst✝¹ : Semiring S
inst✝ : Algebra R S
x✝ : R
⊢ (RingEquiv.sumArrowEquivProdArrow α β S) ((algebraMap R (α ⊕ β → S)) x✝) = (algebraMap R ((α → S) × (β → S))) x✝
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case right
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ -(a • b • s) = (b * c) • t

Tactic:
· rw [mul_smul, neg_eq_iff_add_eq_zero, smul_comm a b, ← smul_add, h₁, smul_zero]

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

Goal state before:
pp: case pos
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : b = 0 ∧ d = 0
hac : a = 0 ∧ c = 0
⊢ ∃ s t, s • a • x + t • c • x = 0 ∧ (s = 0 → t ≠ 0)

pp: case neg
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : b = 0 ∧ d = 0
hac : ¬(a = 0 ∧ c = 0)
⊢ ∃ s t, s • a • x + t • c • x = 0 ∧ (s = 0 → t ≠ 0)

Tactic:
· exact ⟨1, 0, by simp [hac.1, hac.2], by simp⟩

Goal state after:
case neg
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : b = 0 ∧ d = 0
hac : ¬(a = 0 ∧ c = 0)
⊢ ∃ s t, s • a • x + t • c • x = 0 ∧ (s = 0 → t ≠ 0)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case inl
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
c : S
hS : Subsingleton S
⊢ LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]

pp: case inr
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
c : S
hS : Nontrivial S
⊢ LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]

Tactic:
· simp [hS.elim c 0]

Goal state after:
case inr
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
c : S
hS : Nontrivial S
⊢ LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
c : S
⊢ LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]

Tactic:
rcases subsingleton_or_nontrivial S with hS | hS; · simp [hS.elim c 0]
  nontriviality R
  simpa using pair_add_smul_add_smul_iff (x := x) (y := y) 1 0 c 1

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

Goal state before:
pp: A : Type u_1
M : Type u_3
N : Type u_4
inst✝² : AddMonoid A
inst✝¹ : Monoid M
inst✝ : Monoid N
ψ : AddChar A M
hψ : Surjective ⇑ψ
⊢ Injective fun f ↦ f.compAddChar ψ

Tactic:
rintro f g h; rw [DFunLike.ext'_iff] at h ⊢; exact hψ.injective_comp_right h

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
N : Type u_8
inst✝ : AddZeroClass N
f g : R[M] →+ N
hfg : ∀ (m : M), f.comp (singleAddHom m) = g.comp (singleAddHom m)
⊢ ∀ (m : M) (r : R), f (single m r) = g (single m r)

Tactic:
by simpa [DFunLike.ext_iff] using hfg

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Monoid M
motive : R[M] → Prop
x : R[M]
of : ∀ (m : M), motive ((MonoidAlgebra.of R M) m)
add : ∀ (x y : R[M]), motive x → motive y → motive (x + y)
smul : ∀ (r : R) (x : R[M]), motive x → motive (r • x)
⊢ motive (ofCoeff 0)

Tactic:
by simpa using smul 0 (.of R M 1) (of 1)

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝² : Semiring R
x✝ y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝¹ : Monoid M
inst✝ : Monoid N
a : R
x : R[M]
hax : singleOneRingHom a * x = 1
hxa : x * singleOneRingHom a = 1
⊢ x.coeff 1 * a = 1

Tactic:
simpa [coeff_mul_single_one] using congr(($hxa).coeff 1)

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: case H.inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f g₁ g₂ : R[A]
eq : f * g₁ = f * g₂
ih :
  ∀ s ∈ g₁.coeff.support ∪ g₂.coeff.support,
    ∀ {g₁_1 g₂_1 : R[A]},
      (fun x ↦ f * x) g₁_1 = (fun x ↦ f * x) g₂_1 →
        g₁_1.coeff.support ∪ g₂_1.coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase s → g₁_1 = g₂_1
h✝ : (g₁.coeff.support ∪ g₂.coeff.support).Nonempty
hf : f.coeff.support.Nonempty
af : A
haf : af ∈ f.coeff.support
ag : A
hag : ag ∈ g₁.coeff.support ∪ g₂.coeff.support
uniq : UniqueMul f.coeff.support (g₁.coeff.support ∪ g₂.coeff.support) af ag
h : (f * g₁).coeff (af * ag) = f.coeff af * g₁.coeff ag
⊢ g₁ = g₂

Tactic:
rw [eq, coeff_mul_mul_of_uniqueMul (uniq.mono subset_rfl Finset.subset_union_right)] at h

Goal state after:
case H.inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f g₁ g₂ : R[A]
eq : f * g₁ = f * g₂
ih :
  ∀ s ∈ g₁.coeff.support ∪ g₂.coeff.support,
    ∀ {g₁_1 g₂_1 : R[A]},
      (fun x ↦ f * x) g₁_1 = (fun x ↦ f * x) g₂_1 →
        g₁_1.coeff.support ∪ g₂_1.coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase s → g₁_1 = g₂_1
h✝ : (g₁.coeff.support ∪ g₂.coeff.support).Nonempty
hf : f.coeff.support.Nonempty
af : A
haf : af ∈ f.coeff.support
ag : A
hag : ag ∈ g₁.coeff.support ∪ g₂.coeff.support
uniq : UniqueMul f.coeff.support (g₁.coeff.support ∪ g₂.coeff.support) af ag
h : f.coeff af * g₂.coeff ag = f.coeff af * g₁.coeff ag
⊢ g₁ = g₂
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x y : R[G]
g : G
⊢ (x * y).coeff g = x.coeff.sum fun h r ↦ r * y.coeff (h⁻¹ * g)

Tactic:
classical rw [coeff_mul]; gcongr; simp +contextual [← eq_inv_mul_iff_mul_eq]

Goal state after:
Module: Mathlib.Data.Multiset.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Multiset α
r : α → α → Prop
inst✝⁷ : DecidableRel r
inst✝⁶ : IsTrans α r
inst✝⁵ : Std.Antisymm r
inst✝⁴ : Std.Total r
r' : β → β → Prop
inst✝³ : DecidableRel r'
inst✝² : IsTrans β r'
inst✝¹ : Std.Antisymm r'
inst✝ : Std.Total r'
hs : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → (r a b ↔ r' (f a) (f b))
⊢ List.map f (s.sort r) = (map f s).sort r'

Tactic:
by
  revert s
  exact Quot.ind fun l h => map_mergeSort (l := l) (by simpa using h)

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ Subsingleton R → Subsingleton R[X]

Tactic:
intro

Goal state after:
R : Type u
inst✝ : Semiring R
a✝ : Subsingleton R
⊢ Subsingleton R[X]
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a✝ : Subsingleton R
⊢ Subsingleton R[X]

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ Nontrivial R[ℕ]

Tactic:
infer_instance

Goal state after:
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: ι : Type u_5
R : Type u_6
M : Type u_7
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
w : ι → R
⊢ ((piEquiv ι R M) v) w = ∑ i, w i • v i

Tactic:
simp only [piEquiv, Basis.constr_apply_fintype, Basis.equivFun_apply]

Goal state after:
ι : Type u_5
R : Type u_6
M : Type u_7
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
w : ι → R
⊢ ∑ i, ((Pi.basisFun R ι).repr w) i • v i = ∑ i, w i • v i
Module: Mathlib.RingTheory.Finiteness.Cardinality

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite R
s : Finset M
⊢ Module.Finite R ↥(span R ↑s)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_3
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : UniqueProds G
inst✝ : UniqueProds H
⊢ UniqueProds (I G H true)

pp: case refine_1
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : UniqueProds G
inst✝ : UniqueProds H
this : ∀ (b : Bool), UniqueProds (I G H b)
⊢ UniqueProds (G × H)

pp: case refine_2
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : UniqueProds G
inst✝ : UniqueProds H
⊢ UniqueProds (I G H false)

Tactic:
· exact of_injective_mulHom (downMulHom H) down_injective ‹_›

Goal state after:
case refine_1
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : UniqueProds G
inst✝ : UniqueProds H
this : ∀ (b : Bool), UniqueProds (I G H b)
⊢ UniqueProds (G × H)

case refine_2
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : UniqueProds G
inst✝ : UniqueProds H
⊢ UniqueProds (I G H false)
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: σ : Type u_1
inst✝ : Finite σ
⊢ Module.Finite ℤ (FreeAbelianGroup σ)

Tactic:
infer_instance

Goal state after: