mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupInacc (f i)
⊢ DirSupInacc (⋃ i, f i)

Tactic:
by
  rw [← sUnion_range f]
  exact DirSupInacc.sUnion (by simpa)

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝⁴ : LinearOrder α
inst✝³ : WellFoundedLT α
inst✝² : SuccOrder α
inst✝¹ : LinearOrder β
inst✝ : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
⊢ f = g ↔ f ⊥ = g ⊥ ∧ ∀ (a : α), f a = g a → f (succ a) = g (succ a)

Tactic:
constructor
  · simp_all
  rintro ⟨H₁, H₂⟩
  ext a
  induction a using SuccOrder.limitRecOn with
  | isMin a ha => rw [ha.eq_bot, H₁]
  | succ a ha IH => exact H₂ a IH
  | isSuccLimit a ha IH =>
    apply (hf.isLUB_image_Iio_of_isSuccLimit ha).unique
    convert! hg.isLUB_image_Iio_of_isSuccLimit ha using 1
    aesop

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

Goal state before:
pp: s : Set Ordinal.{u}
hf : BddAbove s
f : Ordinal.{u} → Ordinal.{max u v}
⊢ BddAbove (f '' s)

Tactic:
bddAbove_iff_small

Goal state after:
s : Set Ordinal.{u}
hf : Small.{u, u + 1} ↑s
f : Ordinal.{u} → Ordinal.{max u v}
⊢ Small.{max u v, (max u v) + 1} ↑(f '' s)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mpr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : Nonempty (r ≺i s)
f : r ≺i s
⊢ ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≺i ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r

Tactic:
· exact (f.relIsoTrans (RelIso.preimage Equiv.ulift r)).transInitial
      (RelIso.preimage Equiv.ulift s).symm.toInitialSeg

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

Goal state before:
pp: ⊢ enumOrd univ = id

Tactic:
by
  rw [← range_id]
  exact enumOrd_range strictMono_id

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

Goal state before:
pp: n : ℕ
a : Ordinal.{u_4}
⊢ n • a + a = a * ↑(n + 1)

Tactic:
nsmul_eq_mul,

Goal state after:
n : ℕ
a : Ordinal.{u_4}
⊢ a * ↑n + a = a * ↑(n + 1)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ a / 0 = 0

Tactic:
change sSup _ = _

Goal state after:
a : Ordinal.{u_4}
⊢ sSup ((fun x ↦ 0 * x) ⁻¹' Iic a) = 0
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
n : ℕ
⊢ o.card = ↑n ↔ o = ↑n

Tactic:
simp only [le_antisymm_iff, card_le_nat, nat_le_card]

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

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

Tactic:
rcases H with ⟨c, rfl⟩
  rcases eq_or_ne b 0 with (rfl | hb)
  · simp
  · simp [mod_def, hb]

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

Goal state before:
pp: s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
⊢ ¬BddAbove sᶜ

Tactic:
bddAbove_iff_small

Goal state after:
s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
⊢ ¬Small.{u, u + 1} ↑sᶜ
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
h : Small.{u, u + 1} ↑sᶜ
this : Small.{u, u + 1} ↑univ
⊢ False

Tactic:
small_univ_iff

Goal state after:
s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
h : Small.{u, u + 1} ↑sᶜ
this : Small.{u, u + 1} Ordinal.{u}
⊢ False
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a ^ (1 + b) = a * a ^ b

Tactic:
rw [opow_add, opow_one]

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

Goal state before:
pp: n : ℕ
a : Ordinal.{u_4}
ha : a < ↑n + ω
b : Ordinal.{u_4}
hb' : b < ω
hb : a ≤ ↑n + b
⊢ a < ω

Tactic:
obtain ⟨m, rfl⟩ := lt_omega0.1 hb'

Goal state after:
n : ℕ
a : Ordinal.{u_4}
ha : a < ↑n + ω
m : ℕ
hb' : ↑m < ω
hb : a ≤ ↑n + ↑m
⊢ a < ω
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ clog b n ≤ clog c n

Tactic:
clog_le_iff_le_pow (lt_of_lt_of_le hc hb)

Goal state after:
b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ n ≤ b ^ clog c n
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
← lt_add_one_iff,

Goal state after:
case inr.inr
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : 1 < b
⊢ log b o < 0 + 1
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}
⊢ (∀ (i_1 : ↑(Set.Iio o)), f i (derivFamily f ↑i_1) ≤ c) ↔ ∀ (i : ↑(Set.Iio o)), derivFamily f ↑i ≤ c

Tactic:
refine forall_congr' fun a ↦ ?_

Goal state after:
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
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case mpr.a
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ (y + 1)
⊢ log b x ≤ y

Tactic:
← lt_add_one_iff,

Goal state after:
case mpr.a
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ (y + 1)
⊢ log b x < y + 1
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ω ^ log ω a * ↑(n + 1) + a % ω ^ log ω a - ω ^ log ω a < a

Tactic:
rw [add_comm, Nat.cast_add, Nat.cast_one, mul_one_add, add_assoc, Ordinal.add_sub_cancel]
    apply (opow_mul_add_lt_opow_mul _ (lt_add_one _)).trans_le
    · rw [Ordinal.mul_le_iff_le_div, hn] <;> simp
    · exact mod_lt _ (opow_ne_zero _ omega0_ne_zero)

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

Goal state before:
pp: a o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
ha : a < o
n : ℕ
⊢ a * ↑n < o

Tactic:
by
  induction n with
  | zero => simpa using ha.pos
  | succ n h =>
    rw [Nat.cast_add_one, mul_add_one]
    exact ho h ha

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

Goal state before:
pp: c : Cardinal.{u_1}
IH : ∀ y < c, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ c
⊢ c ≤ c * c

Tactic:
by simpa using mul_le_mul_right (one_le_aleph0.trans hc) c

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

Goal state before:
pp: case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 0 < b
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (a * b)

Tactic:
rw [← one_le_iff_pos] at hb₁'
      intro c d hc hd
      rw [lt_mul_iff_of_isSuccLimit
        (isSuccLimit_of_isPrincipal_add (lt_of_le_of_ne hb₁' hb₁.symm) hb)] at *
      rcases hc with ⟨x, hx, hx'⟩
      rcases hd with ⟨y, hy, hy'⟩
      use x + y, hb hx hy
      rw [mul_add]
      exact Left.add_lt_add hx' hy'

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

Goal state before:
pp: case a
o : Ordinal.{u}
h : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a ≤ 1

Tactic:
← lt_add_one_iff,

Goal state after:
case a
o : Ordinal.{u}
h : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a < 1 + 1
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.cof ≤ 1 ↔ ¬IsSuccLimit o

Tactic:
Cardinal.le_one_iff,

Goal state after:
o : Ordinal.{u_1}
⊢ o.cof = 0 ∨ o.cof = 1 ↔ ¬IsSuccLimit o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr.inl
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ succ c
⊢ a * b < ω ^ succ c

Tactic:
rw [opow_succ] at ha
    obtain ⟨n, hn, an⟩ :=
      ((isNormal_mul_right <| opow_pos _ omega0_pos).lt_iff_exists_lt isSuccLimit_omega0).1 ha
    grw [an, opow_succ, mul_assoc]
    gcongr
    exacts [opow_pos _ omega0_pos, isPrincipal_mul_omega0 hn hb]

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

Goal state before:
pp: case inr
α : Type u
h✝ : Infinite α
⊢ #(List α) ≤ max ℵ₀ #α

Tactic:
rw [mk_list_eq_mk]

Goal state after:
case inr
α : Type u
h✝ : Infinite α
⊢ #α ≤ max ℵ₀ #α
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, y < c.ord → preBeth y < c
ha : a < c.ord
⊢ lift.{u_1 + 1, u_1} a.card < (lift.{u_1 + 1, u_1} c).ord.cof

Tactic:
hc.isRegular.lift.cof_ord,

Goal state after:
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, y < c.ord → preBeth y < c
ha : a < c.ord
⊢ lift.{u_1 + 1, u_1} a.card < lift.{u_1 + 1, u_1} c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ℶ_ c.ord = c

Tactic:
← preBeth_of_omega0_sq_le (le_of_lt _),

Goal state after:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ preBeth c.ord = c

c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ω ^ 2 < c.ord
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ preBeth c.ord = c

pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ω ^ 2 < c.ord

Tactic:
hc.preBeth_ord

Goal state after:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ c = c

c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ω ^ 2 < c.ord
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
⊢ Trunc { s // ∀ (i : ι), i ∈ s ∨ f i (x i) (y i) = 0 }

Tactic:
refine x.support'.bind fun xs => ?_
    refine y.support'.map fun ys => ?_
    refine ⟨xs + ys, fun i => ?_⟩
    obtain h1 | (h1 : x i = 0) := xs.prop i
    · grind
    obtain h2 | (h2 : y i = 0) := ys.prop i
    · grind
    grind

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
⊢ f = 0 → f.support = ∅

Tactic:
by simp +contextual

Goal state after:
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
ι : Sort u_3
U : ι → Submodule R M
⊢ ⨆ i, (U i).dualAnnihilator ≤ (⨅ i, U i).dualAnnihilator

Tactic:
rw [le_dualAnnihilator_iff_le_dualCoannihilator, dualCoannihilator_iSup_eq]
  apply iInf_mono
  exact fun i : ι => le_dualAnnihilator_dualCoannihilator (U i)

Goal state after:
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
s : Set (Dual R M)
x : M
this : ∀ (φ : M →ₗ[R] R), x ∈ φ.ker ↔ φ ∈ LinearMap.ker ((Dual.eval R M) x)
⊢ x ∈ ↑(span R s).dualCoannihilator ↔ x ∈ {x | ∀ f ∈ s, f x = 0}

Tactic:
simp only [SetLike.mem_coe, mem_dualCoannihilator, Set.mem_ofPred_eq, ← LinearMap.mem_ker, this]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Dual R M)
x : M
this : ∀ (φ : M →ₗ[R] R), x ∈ φ.ker ↔ φ ∈ LinearMap.ker ((Dual.eval R M) x)
⊢ (∀ φ ∈ span R s, φ ∈ LinearMap.ker ((Dual.eval R M) x)) ↔ ∀ f ∈ s, f ∈ LinearMap.ker ((Dual.eval R M) x)
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mp
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0
s : Finset ι
v : ι → N
hv : ∀ i ∈ s, v i ∈ p i
⊢ ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0

Tactic:
hv0

Goal state after:
case mp
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0
s : Finset ι
v : ι → N
hv : ∀ i ∈ s, v i ∈ p i
hv0 : ∑ i ∈ s, v i = 0
⊢ ∀ i ∈ s, v i = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mp
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0
s : Finset ι
v : ι → N
hv : ∀ i ∈ s, v i ∈ p i
i : ι
hv0 : -v i = ∑ x ∈ s.erase i, v x
hi : i ∈ s
⊢ -v i ∈ ⨆ j, ⨆ (_ : j ≠ i), p j

Tactic:
hv0

Goal state after:
case mp
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0
s : Finset ι
v : ι → N
hv : ∀ i ∈ s, v i ∈ p i
i : ι
hv0 : -v i = ∑ x ∈ s.erase i, v x
hi : i ∈ s
⊢ ∑ x ∈ s.erase i, v x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case refine_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
u v : R
hu : IsUnit u
hv : IsUnit v
h : ∀ (s t : R), s • u • x + t • v • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ s = 0 ∧ t = 0

pp: case refine_2
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
u v : R
hu : IsUnit u
hv : IsUnit v
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • v • y = 0
⊢ s = 0 ∧ t = 0

Tactic:
· specialize h (s * hu.unit⁻¹) (t * hv.unit⁻¹)
    simp only [Units.mul_left_eq_zero] at h
    apply h
    simpa [← mul_smul, mul_assoc]

Goal state after:
case refine_2
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
u v : R
hu : IsUnit u
hv : IsUnit v
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • v • y = 0
⊢ s = 0 ∧ t = 0
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval - l₂.eval = l.eval
⊢ a₁.1 • a₁.2 + l₁.eval + -(a₂.1 • a₂.2) = -(a₂.1 • a₂.2) + a₁.1 • a₁.2 + l₁.eval

Tactic:
rw [add_comm, add_assoc]

Goal state after:
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
l : NF R M
x : M
h : x = l.eval
r : R
⊢ (r • l).eval = r • x

Tactic:
by
  unfold NF.eval at h ⊢
  simp only [h, smul_sum, map_map, NF.smul_apply]
  congr
  ext p
  simp [mul_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (s : Finset ι) (v w : ι → N), (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i
s : Finset ι
v : ι → N
hv : ∀ i ∈ s, v i ∈ p i
⊢ ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0

Tactic:
hv0

Goal state after:
case mpr
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (s : Finset ι) (v w : ι → N), (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i
s : Finset ι
v : ι → N
hv : ∀ i ∈ s, v i ∈ p i
hv0 : ∑ i ∈ s, v i = 0
⊢ ∀ i ∈ s, v i = 0
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
f : X →₀ ℤ
⊢ toFinsupp (toFreeAbelianGroup f) = f

Tactic:
by
  rw [← AddMonoidHom.comp_apply, toFinsupp_comp_toFreeAbelianGroup, AddMonoidHom.id_apply]

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

Goal state before:
pp: case empty
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
ψ : ι → AddChar A M
⊢ ⇑(∏ i ∈ ∅, ψ i) = ∏ i ∈ ∅, ⇑(ψ i)

Tactic:
simp [*]

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

Goal state before:
pp: case cons
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
ψ : ι → AddChar A M
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ⇑(∏ i ∈ s✝, ψ i) = ∏ i ∈ s✝, ⇑(ψ i)
⊢ ⇑(∏ i ∈ cons a✝¹ s✝ h✝, ψ i) = ∏ i ∈ cons a✝¹ s✝ h✝, ⇑(ψ i)

Tactic:
simp [*]

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

Goal state before:
pp: case empty
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
ψ : ι → AddChar A M
⊢ ⇑(∑ i ∈ ∅, ψ i) = ∏ i ∈ ∅, ⇑(ψ i)

Tactic:
simp [*]

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

Goal state before:
pp: case cons
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
ψ : ι → AddChar A M
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ⇑(∑ i ∈ s✝, ψ i) = ∏ i ∈ s✝, ⇑(ψ i)
⊢ ⇑(∑ i ∈ cons a✝¹ s✝ h✝, ψ i) = ∏ i ∈ cons a✝¹ s✝ h✝, ⇑(ψ i)

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
u : Finset γ
⊢ image₂ f s t ⊆ u ↔ ∀ a ∈ s, image (fun b ↦ f a b) t ⊆ u

Tactic:
by
  simp_rw [image₂_subset_iff, image_subset_iff]

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

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
⊢ ∃ b ⊆ t, s ⊆ b ∧ v '' t ⊆ ↑(span K (v '' b)) ∧ LinearIndepOn K v b

Tactic:
by
  obtain ⟨b, sb, h⟩ := by
    refine zorn_subset_nonempty { b | b ⊆ t ∧ LinearIndepOn K v b} ?_ _ ⟨hst, hs⟩
    · refine fun c hc cc _c0 => ⟨⋃₀ c, ⟨?_, ?_⟩, fun x => ?_⟩
      · exact sUnion_subset fun x xc => (hc xc).1
      · exact linearIndepOn_sUnion_of_directed cc.directedOn fun x xc => (hc xc).2
      · exact subset_sUnion_of_mem
  refine ⟨b, h.prop.1, sb, fun _ ⟨x, hx, hvx⟩ => by_contra fun hn ↦ hn ?_, h.prop.2⟩
  subst hvx
  exact subset_span <| mem_image_of_mem v <| h.mem_of_prop_insert
    ⟨insert_subset hx h.prop.1, h.prop.2.insert hn⟩

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

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
r : R
n : N
hn : n ∉ Set.range f
hf : Injective f
a✝ : M
⊢ (comapDomain f hf (single n r)).coeff a✝ = (coeff 0) a✝

Tactic:
simp [*]

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

Goal state before:
pp: case pos
α : 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
h : Disjoint (image (f a) t) (image₂ f s t)
⊢ #t ∣ #(image (fun b ↦ f a b) t ∪ image₂ f s t)

Tactic:
rw [card_union_of_disjoint h]
    exact Nat.dvd_add (card_image_of_injective _ <| hf _ <| mem_insert_self _ _).symm.dvd ih

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

Goal state before:
pp: case pos
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
x : V
h✝ : x ∈ s
⊢ x ∈ {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} ↔ x ∈ t

Tactic:
simp [*]

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

Goal state before:
pp: case neg
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
x : V
h✝ : x ∉ s
⊢ x ∈ {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} ↔ x ∈ t

Tactic:
simp [*]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
r : R
m : M
⊢ single m r = 0 ↔ r = 0

Tactic:
by simp [← coeff_inj]

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

Goal state before:
pp: ι : Type u_14
α : ι → Type u_15
β : ι → Type u_16
γ : ι → Type u_17
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → α i → β i → γ i
s : (i : ι) → Finset (α i)
t : (i : ι) → Finset (β i)
⊢ (piFinset fun i ↦ image₂ (f i) (s i) (t i)) = image₂ (fun a b i ↦ f i (a i) (b i)) (piFinset s) (piFinset t)

Tactic:
by
  ext; simp only [mem_piFinset, mem_image₂, Classical.skolem, forall_and, funext_iff]

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

Goal state before:
pp: case h
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
x : R[M]
r : R
m m₁ : M
inst✝ : Mul M
m₂ : M
H : ∀ m' ∈ x.coeff.support, m' * m = m₁ ↔ m' = m₂
m' : M
a✝ : m' ∈ x.coeff.support
⊢ (if m' * m = m₁ then x.coeff m' * r else 0) = if m' = m₂ then x.coeff m' * r else 0

Tactic:
simp [*]

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

Goal state before:
pp: case h
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
x : R[M]
r : R
m m₁ : M
inst✝ : Mul M
m₂ : M
H : ∀ m' ∈ x.coeff.support, m * m' = m₁ ↔ m' = m₂
m' : M
a✝ : m' ∈ x.coeff.support
⊢ (if m * m' = m₁ then r * x.coeff m' else 0) = if m' = m₂ then r * x.coeff m' else 0

Tactic:
simp [*]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Mul G
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
⊢ UniqueMul A B a0 b0 ↔ #({p ∈ A ×ˢ B | p.1 * p.2 = a0 * b0}) ≤ 1

Tactic:
by
  simp_rw [card_le_one_iff, mem_filter, mem_product]
  refine ⟨fun h p1 p2 ⟨⟨ha1, hb1⟩, he1⟩ ⟨⟨ha2, hb2⟩, he2⟩ ↦ ?_, fun h a b ha hb he ↦ ?_⟩
  · have h1 := h ha1 hb1 he1; have h2 := h ha2 hb2 he2
    grind
  · exact Prod.ext_iff.1 (@h (a, b) (a0, b0) ⟨⟨ha, hb⟩, he⟩ ⟨⟨ha0, hb0⟩, rfl⟩)

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

Goal state before:
pp: α : Type u_1
s : Finset α
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : Std.Antisymm r
inst✝ : Std.Total r
⊢ (↑(s.sort r)).Nodup

Tactic:
rw [sort_eq]

Goal state after:
α : Type u_1
s : Finset α
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : Std.Antisymm r
inst✝ : Std.Total r
⊢ s.val.Nodup
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
⊢ UniqueMul (map { toFun := op, inj' := ⋯ } (map { toFun := op, inj' := ⋯ } A))
    (map { toFun := op, inj' := ⋯ } (map { toFun := op, inj' := ⋯ } B)) (op (op a0)) (op (op b0))

Tactic:
map_map

Goal state after:
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
⊢ UniqueMul (map ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) A)
    (map ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) B) (op (op a0)) (op (op b0))
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
⊢ 1 < #A ∨ 1 < #B

Tactic:
exact hc.2.2

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : End R M
e : M ≃ₗ[R] N
p : Submodule R M
⊢ Submodule.map (↑e) p ∈ (e.conj f).invtSubmodule ↔ p ∈ f.invtSubmodule

Tactic:
have : e.symm.toLinearMap ∘ₗ ((e ∘ₗ f) ∘ₗ e.symm.toLinearMap) ∘ₗ e = f := by ext; simp
  rw [LinearEquiv.conj_apply, mem_invtSubmodule, mem_invtSubmodule, Submodule.map_le_iff_le_comap,
    Submodule.map_equiv_eq_comap_symm, ← Submodule.comap_comp, ← Submodule.comap_comp, this]

Goal state after: