mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : g.Finite
hf : f.Finite
⊢ (g.comp f).Finite

Tactic:
algebraize [f, g, g.comp f]

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : g.Finite
hf : f.Finite
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
algebraizeInst✝¹ : Module.Finite B C
algebraizeInst✝ : Module.Finite A B
⊢ (g.comp f).Finite
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : (g.comp f).Finite
⊢ g.Finite

Tactic:
algebraize [f, g, g.comp f]

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : (g.comp f).Finite
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
algebraizeInst✝ : Module.Finite A C
⊢ g.Finite
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulReflectLE α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 < a
b₁ b₂ : β
h : a • b₁ ≤ a • b₂
⊢ a • f b₁ ≤ a • f b₂

Tactic:
simpa only [smul] using hf.2 h

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 : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
a : Ordinal.{u}
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < a
⊢ liftInitialSeg.toRelEmbedding a = lift.{max (u + 1) v, max (u + 1) v} (type s)

Tactic:
induction a using inductionOn with | type α r
       =>  _ 

Goal state after:
case mpr.type
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})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
⊢ liftInitialSeg.toRelEmbedding (type r) = lift.{max (u + 1) v, max (u + 1) v} (type s)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsSuccLimit (type r)
x b : α
hb : b ∈ {x}
⊢ r b ((enum r) ⟨succ ((typein r).toRelEmbedding x), ⋯⟩)

Tactic:
mem_singleton_iff.1 hb

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsSuccLimit (type r)
x b : α
hb : b ∈ {x}
⊢ r x ((enum r) ⟨succ ((typein r).toRelEmbedding x), ⋯⟩)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
h0 : 0 < type r
a : α
⊢ ⟨0, h0⟩ ≤ ⟨(typein r).toRelEmbedding a, ⋯⟩

Tactic:
exact bot_le (α := Ordinal)

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c a b : Ordinal.{u}
⊢ (fun x1 x2 ↦ x1 ≤ x2) a b →
    (fun x1 x2 ↦ x1 ≤ x2) (Function.swap (fun x1 x2 ↦ x1 + x2) c a) (Function.swap (fun x1 x2 ↦ x1 + x2) c b)

Tactic:
refine inductionOn₃ a b c fun α r _ β s _ γ t _ ⟨f⟩ ↦
      (RelEmbedding.ofMonotone (Sum.recOn · (Sum.inl ∘ f) Sum.inr) ?_).ordinal_type_le
    simp [f.map_rel_iff]

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

Goal state before:
pp: case mpr
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
⊢ StrictMono f ∧ range f = s → enumOrd s = f

Tactic:
rintro ⟨h₁, h₂⟩

Goal state after:
case mpr
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
h₁ : StrictMono f
h₂ : range f = s
⊢ enumOrd s = f
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr
b x y : ℕ
hx : x ≠ 0
hlt : y < b ^ x
hy : y ≠ 0
⊢ log b y < x

Tactic:
· exact log_lt_of_lt_pow hy hlt

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

Goal state before:
pp: case cons.cons
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun x1 x2 ↦ x1 < x2) (b :: bs) (a :: as)
⊢ ∀ i ∈ b :: bs, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o

Tactic:
intro i hi
      suffices h : i ≤ a by refine lt_of_le_of_lt ?_ (hlt a mem_cons_self); simpa
      cases hi with
      | head as => exact List.head_le_of_lt hmltl
      | tail b hi => exact le_of_lt (lt_of_lt_of_le (List.rel_of_pairwise_cons hm.pairwise hi)
          (List.head_le_of_lt hmltl))

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ c ^ log b n ≤ n

Tactic:
calc
    c ^ log b n ≤ b ^ log b n := Nat.pow_le_pow_left hb _
    _ ≤ n := pow_log_le_self _ hn

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

Goal state before:
pp: a b c : Ordinal.{u_4}
⊢ a < b * c ↔ ∃ q < c, ∃ r < b, a = b * q + r

Tactic:
obtain rfl | hb₀ := eq_or_ne b 0; · simp
  refine ⟨fun h ↦ ⟨_, (lt_mul_iff_div_lt hb₀).1 h, _, mod_lt a hb₀, (div_add_mod ..).symm⟩, ?_⟩
  rintro ⟨q, hq, r, hr, rfl⟩
  grw [hr, ← mul_add_one, add_one_le_iff.2 hq]

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

Goal state before:
pp: case inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
⊢ a ^ 1 ≤ a ^ b

pp: case inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : 1 < a
⊢ a ^ 1 ≤ a ^ b

Tactic:
· rcases lt_or_eq_of_le a1 with a0 | a1
    · rw [lt_one_iff] at a0
      rw [a0, zero_opow one_ne_zero]
      exact zero_le
    rw [a1, one_opow, one_opow]

Goal state after:
case inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : 1 < a
⊢ a ^ 1 ≤ a ^ b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ 1 + c = c

Tactic:
← card_ord c,

Goal state after:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ 1 + c.ord.card = c.ord.card
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a : Ordinal.{u_1}
ha : 0 < a
⊢ nfp (fun x ↦ a * x) 1 = a ^ ω

Tactic:
by
  rw [← iSup_iterate_eq_nfp, ← iSup_pow_natCast ha]
  simp

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

Goal state before:
pp: o₁ o₂ : Ordinal.{u_1}
⊢ ℵ_ o₁ * ℵ_ o₂ = ℵ_ (max o₁ o₂)

Tactic:
Cardinal.mul_eq_max (aleph0_le_aleph o₁) (aleph0_le_aleph o₂),

Goal state after:
o₁ o₂ : Ordinal.{u_1}
⊢ max (ℵ_ o₁) (ℵ_ o₂) = ℵ_ (max o₁ o₂)
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
i j : Ordinal.{u}
hi : i < o
hj : j < o
hij : i ≤ j
⊢ f i hi ≤ f j hj

Tactic:
by
  rcases lt_or_eq_of_le hij with (hij | rfl)
  · exact (hf.2.1 hi hj hij).le
  · rfl

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
⊢ nfpFamily f a < c

Tactic:
by
  refine lift_iSup_lt_of_lt_cof ?_ (fun l ↦ ?_)
  · rw [Cardinal.lift_umax, c.lift_id']
    apply (Cardinal.lift_le.2 (mk_list_le_max _)).trans_lt
    rw [Cardinal.lift_max]
    apply max_lt <;> simpa
  · induction l with
    | nil => exact ha
    | cons i l H => exact hf _ _ H

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a.card < c
hb : b.card < c
⊢ ((fun x1 x2 ↦ x1 + x2) a b).card < c

Tactic:
card_add

Goal state after:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a.card < c
hb : b.card < c
⊢ a.card + b.card < c
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a.card < c
hb : b.card < c
⊢ a.card + b.card < c

Tactic:
exact add_lt_of_lt hc ha hb

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

Goal state before:
pp: α : Type u
r : α → α → Prop
H : IsWellOrder α r
h : IsSuccLimit (type r)
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : WellFoundedLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : #↑s = Order.cof α
⊢ ∀ (a : α), ∃ b ∈ s, r a b

Tactic:
← not_bddAbove_iff_isCofinal,

Goal state after:
α : Type u
r : α → α → Prop
H : IsWellOrder α r
h : IsSuccLimit (type r)
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : WellFoundedLT α
this : NoMaxOrder α
s : Set α
hs : ¬BddAbove s
hs' : #↑s = Order.cof α
⊢ ∀ (a : α), ∃ b ∈ s, r a b
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h : Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x

Tactic:
have := h

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h this : Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
i : ι
f : Π₀ (i : ι), β i
i' : ι
h : ¬i = i'
⊢ (erase i f + single i (f i)) i' = f i'

Tactic:
by
      simp only [add_apply, single_apply, erase_apply, dif_neg h, if_neg (Ne.symm h), add_zero]

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddGroup (β i)
s : Finset ι
x y : (i : ↑↑s) → β ↑i
i : ι
⊢ (mk s (x - y)) i = (mk s x - mk s y) i

Tactic:
simp only [sub_apply, mk_apply]

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddGroup (β i)
s : Finset ι
x y : (i : ↑↑s) → β ↑i
i : ι
⊢ (if H : i ∈ s then (x - y) ⟨i, H⟩ else 0) = (if H : i ∈ s then x ⟨i, H⟩ else 0) - if H : i ∈ s then y ⟨i, H⟩ else 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case some
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
⊢ (extendWith 0 (single i x)) (some j) = (single (some i) x) (some j)

Tactic:
rw [extendWith_some]

Goal state after:
case some
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
⊢ (single i x) j = (single (some i) x) (some j)
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁸ : CommSemiring K
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module K V
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
r : R
hr : IsRegular r
m₁ m₂ : M
hm : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
n : Dual R M
⊢ ((Dual.eval R M) m₁) n = ((Dual.eval R M) m₂) n

Tactic:
simpa [hr.1.eq_iff] using congr(n $hm)

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
m : Π₀ (i : ι), ↥(p i)
hm : ((lsum ℕ) fun i ↦ (p i).subtype) m = 0
i : ι
⊢ m i = 0 i

Tactic:
rw [DFinsupp.zero_apply, ← neg_eq_zero]

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
m : Π₀ (i : ι), ↥(p i)
hm : ((lsum ℕ) fun i ↦ (p i).subtype) m = 0
i : ι
⊢ -m i = 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
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
⊢ LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ a * d ≠ b * c

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
a b c d : S
inst✝ : Nontrivial R
h : a * d ≠ b * c
⊢ LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ a * d ≠ b * c

Tactic:
· suffices ¬ LinearIndependent R ![a • x + b • y, c • x + d • y] by simpa [h]
    rw [pair_iff]
    push Not
    by_cases hbd : b = 0 ∧ d = 0
    · simp only [hbd.1, hbd.2, zero_smul, add_zero]
      by_cases hac : a = 0 ∧ c = 0; · exact ⟨1, 0, by simp [hac.1, hac.2], by simp⟩
      refine ⟨c • 1, -a • 1, ?_, by aesop⟩
      simp only [smul_assoc, one_smul, neg_smul]
      module
    refine ⟨d • 1, -b • 1, ?_, by contrapose! hbd; simp_all⟩
    simp only [smul_add, smul_assoc, one_smul, smul_smul, mul_comm d, h]
    module

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
a b c d : S
inst✝ : Nontrivial R
h : a * d ≠ b * c
⊢ LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ a * d ≠ b * c
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
inst✝³ : Semiring S
inst✝² : DistribSMul R S
inst✝¹ : Mul M
inst✝ : SMulCommClass R S S
t : R
a b : S[M]
⊢ t • a • b = a • t • b

Tactic:
classical ext; simp [coeff_mul, sum_smul_index', Finsupp.smul_sum, mul_smul_comm]

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

Goal state before:
pp: R : Type u_6
K : Type u_7
M : Type u_8
inst✝⁷ : CommRing R
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R K
inst✝³ : Module K M
inst✝² : Module R M
inst✝¹ : IsScalarTower R K M
inst✝ : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : y ∈ span R (range v)
heq : c • x + y = 0
hc : ¬c = 0
⊢ False

Tactic:
apply hx

Goal state after:
R : Type u_6
K : Type u_7
M : Type u_8
inst✝⁷ : CommRing R
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R K
inst✝³ : Module K M
inst✝² : Module R M
inst✝¹ : IsScalarTower R K M
inst✝ : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : y ∈ span R (range v)
heq : c • x + y = 0
hc : ¬c = 0
⊢ x ∈ span K (range v)
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
f : γ → β → δ
g : α → γ
⊢ image2 f (g '' ↑s) ↑t = image2 (fun a b ↦ f (g a) b) ↑s ↑t

Tactic:
exact image2_image_left _ _

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

Goal state before:
pp: case insert
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : (∀ a ∈ s, Injective (f a)) → ((fun a ↦ image (f a) t) '' ↑s).PairwiseDisjoint id → #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a ↦ image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
⊢ #t ∣ #(image₂ f (insert a s) t)

Tactic:
specialize ih (forall_of_forall_insert hf)
    (hs.subset <| Set.image_mono <| coe_subset.2 <| subset_insert _ _)

Goal state after:
case insert
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a ↦ image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
⊢ #t ∣ #(image₂ f (insert a s) t)
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Monoid M
f : R →+* S
⊢ map (↑f) 1 = 1

Tactic:
ext; simp [one_def]

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

Goal state before:
pp: 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✝ : Semigroup M
⊢ ∀ (a b c : R[M]), a * b * c = a * (b * c)

Tactic:
simp [mul_def, sum_sum_index, mul_add, add_mul, mul_assoc]

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

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
hA1 : #A ≤ 1
hB1 : #B ≤ 1
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
by
  rw [Finset.card_le_one_iff] at hA1 hB1
  obtain ⟨a, ha⟩ := hA; obtain ⟨b, hb⟩ := hB
  exact ⟨a, ha, b, hb, fun _ _ ha' hb' _ ↦ ⟨hA1 ha' ha, hB1 hb' hb⟩⟩

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

Goal state before:
pp: case refine_1
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
inst✝ : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : f aG = aH
hbe : f bG = bH
huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG
a b : G
huH : aH * bH = aH * bH → f a = aH ∧ f b = bH
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ a ∈ A ∧ f a = aH

pp: case refine_2
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
inst✝ : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : f aG = aH
hbe : f bG = bH
huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG
a b : G
huH : aH * bH = aH * bH → f a = aH ∧ f b = bH
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ b ∈ B ∧ f b = bH

Tactic:
exacts [⟨ha, (huH rfl).1⟩, ⟨hb, (huH rfl).2⟩]

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : (s.sort fun a b ↦ a ≤ b).length - 1 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
l : List α := ⋯
⊢ (s.sort fun a b ↦ a ≤ b)[(s.sort fun a b ↦ a ≤ b).length - 1] ≤ s.max' H

pp: case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : (s.sort fun a b ↦ a ≤ b).length - 1 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
l : List α := ⋯
⊢ s.max' H ≤ (s.sort fun a b ↦ a ≤ b)[(s.sort fun a b ↦ a ≤ b).length - 1]

Tactic:
· have : l.get ⟨s.sort.length - 1, h⟩ ∈ s :=
      (s.mem_sort (· ≤ ·)).1 (List.get_mem l _)
    exact s.le_max' _ this

Goal state after:
case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : (s.sort fun a b ↦ a ≤ b).length - 1 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
l : List α := ⋯
⊢ s.max' H ≤ (s.sort fun a b ↦ a ≤ b)[(s.sort fun a b ↦ a ≤ b).length - 1]
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Mul α
inst✝¹ : IsRightCancelMul α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
hc : c ∈ t
⊢ (s * t).Nontrivial

Tactic:
exact ⟨a * c, mul_mem_mul ha hc, b * c, mul_mem_mul hb hc, by simpa⟩

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
m n : ℕ
a b : R
⊢ (monomial m) a = (monomial n) b ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0

Tactic:
← toFinsupp_inj,

Goal state after:
R : Type u
inst✝ : Semiring R
m n : ℕ
a b : R
⊢ ((monomial m) a).toFinsupp = ((monomial n) b).toFinsupp ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ p * X ^ n * q = p * q * X ^ n

Tactic:
rw [mul_assoc, X_pow_mul, ← mul_assoc]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (p.update n a).coeff n = a

Tactic:
by
  rw [p.coeff_update_apply, if_pos rfl]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.update n 0).support = p.support.erase n

Tactic:
by
  rw [update_zero_eq_erase, support_erase]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
ha : a ≠ 0
⊢ (p.update n a).support = insert n p.support

Tactic:
rw [support_update, if_neg ha]

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

Goal state before:
pp: case neg
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), UniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B✝ : Finset ((i : ι) → G i)
hA✝ : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB✝ : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
hc :
  (1 < #(image (fun x ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A) ∨
    1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
ai : G i
hA : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) ai bi
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
let A' := {a ∈ A | a i = ai}

Goal state after:
case neg
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), UniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B✝ : Finset ((i : ι) → G i)
hA✝ : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB✝ : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
hc :
  (1 < #(image (fun x ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A) ∨
    1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
ai : G i
hA : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) ai bi
A' : Finset ((i : ι) → G i) := {a ∈ A | a i = ai}
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0