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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : WellFoundedLT α
inst✝⁴ : SuccOrder α
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ y, x ≤ f y
hx : f ⊥ ≤ x
this✝² : Nonempty β
this✝¹ : OrderBot β := WellFoundedLT.toOrderBot β
this✝ : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
H : BddAbove (f ⁻¹' Iic x)
⊢ x < f (succ (sSup (f ⁻¹' Iic x)))

Tactic:
rw [← not_le, hf.le_iff_le_sSup ⟨⊥, hx⟩ H, not_le, lt_succ_iff]

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a b : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝⁵ : IsWellOrder α r
β : Type u
s : β → β → Prop
x✝⁴ : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
x✝³ : IsWellOrder γ t
x✝² : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), f (Sum.inl a) = Sum.inl a
g : α → β
hg : ∀ (a : α), f (Sum.inr a) = Sum.inr (g a)
x✝¹ x✝ : α
h : r x✝¹ x✝
⊢ s (g x✝¹) (g x✝)

Tactic:
← @Sum.lex_inr_inr _ t _ s,

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a b : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝⁵ : IsWellOrder α r
β : Type u
s : β → β → Prop
x✝⁴ : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
x✝³ : IsWellOrder γ t
x✝² : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), f (Sum.inl a) = Sum.inl a
g : α → β
hg : ∀ (a : α), f (Sum.inr a) = Sum.inr (g a)
x✝¹ x✝ : α
h : r x✝¹ x✝
⊢ Sum.Lex t s (Sum.inr (g x✝¹)) (Sum.inr (g x✝))
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
simpa only [add_zero] using add_sub_cancel a 0

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

Goal state before:
pp: β : Type u_2
f : β → Ordinal.{u}
⊢ BddAbove (range fun i ↦ f i + 1) ↔ BddAbove (range f)

Tactic:
range_comp' (· + 1),

Goal state after:
β : Type u_2
f : β → Ordinal.{u}
⊢ BddAbove ((fun x ↦ x + 1) '' range f) ↔ BddAbove (range f)
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
⊢ enumOrd s o ≤ a

Tactic:
trans ⨆ b : Iio o, enumOrd s b

Goal state after:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
⊢ enumOrd s o ≤ ⨆ b, enumOrd s ↑b

s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
⊢ ⨆ b, enumOrd s ↑b ≤ a
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_1
α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
o : Ordinal.{u}
⊢ (o ∈ range fun r ↦ type ↑r) → o ∈ range fun r ↦ type ↑r

Tactic:
rintro ⟨⟨r, hr⟩, rfl⟩

Goal state after:
case refine_1
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
r : α → α → Prop
hr : IsWellOrder α r
⊢ (fun r ↦ type ↑r) ⟨r, hr⟩ ∈ range fun r ↦ type ↑r
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_2
α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
o : Ordinal.{u}
⊢ (o ∈ range fun r ↦ type ↑r) → o ∈ range fun r ↦ type ↑r

Tactic:
rintro ⟨⟨r, hr⟩, rfl⟩

Goal state after:
case refine_2
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
r : β → β → Prop
hr : IsWellOrder β r
⊢ (fun r ↦ type ↑r) ⟨r, hr⟩ ∈ range fun r ↦ type ↑r
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ b * c % b = 0

Tactic:
simp [mod_def, hb]

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

Goal state before:
pp: a b c : Ordinal.{u_1}
h₁ : 0 < a
h₂ : b ≤ c
⊢ a ^ b ≤ a ^ c

Tactic:
by
  rcases (one_le_iff_pos.2 h₁).eq_or_lt' with h₁ | h₁
  · simp_all
  · exact (opow_le_opow_iff_right h₁).2 h₂

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : ℕ
h : (↑a).ord = (↑b).ord
⊢ a = b

Tactic:
Cardinal.ord_inj,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : ℕ
h : ↑a = ↑b
⊢ a = b
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ x < b ^ succ (log b x)

Tactic:
lt_opow_iff_log_lt hb hx,

Goal state after:
case inr
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ log b x < succ (log b x)
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 + 1

Tactic:
← lt_opow_iff_log_lt hb hx

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)
⊢ x < b ^ (y + 1)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: x✝ : Ordinal.{u_1}
⊢ ⨆ n, id^[n] x✝ = id x✝

Tactic:
iterate_id

Goal state after:
x✝ : Ordinal.{u_1}
⊢ ⨆ n, id x✝ = id x✝
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b : Ordinal.{u_1}
ha : a < ω ^ succ b
⊢ ∃ n, a < ω ^ b * ↑n

Tactic:
obtain ⟨c, hc, n, hn⟩ := (lt_omega0_opow (add_pos_of_right zero_lt_one b).ne').1 ha

Goal state after:
a b : Ordinal.{u_1}
ha : a < ω ^ succ b
c : Ordinal.{u_1}
hc : c < b + 1
n : ℕ
hn : a < ω ^ c * ↑n
⊢ ∃ n, a < ω ^ b * ↑n
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_1
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
⊢ a + o = o

pp: case refine_2
o : Ordinal.{u}
h : ∀ a < o, a + o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun x1 x2 ↦ x1 + x2) a b < o

Tactic:
· rcases lt_or_ge 1 o with ho₁ | ho₁
    · exact op_eq_self_of_isPrincipal hao (isNormal_add_right a) ho
        (isSuccLimit_of_isPrincipal_add ho₁ ho)
    · cases le_one_iff.1 ho₁ <;> simp_all

Goal state after:
case refine_2
o : Ordinal.{u}
h : ∀ a < o, a + o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun x1 x2 ↦ x1 + x2) a b < o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a b c : Ordinal.{u}
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
hab : a < b
hbc : b ≤ c
⊢ a + c = c

Tactic:
rw [← Ordinal.add_sub_cancel_of_le hbc, ← add_assoc, hb.add_eq_right hab,
    Ordinal.add_sub_cancel_of_le hbc]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.Countable ↔ #↑s < ℵ_ 1

Tactic:
rw [lt_aleph_one_iff, le_aleph0_iff_set_countable]

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

Goal state before:
pp: case inr.a
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
x : Ordinal.{u}
xb : x < ω ^ b
ax : a < ω ^ x
⊢ a * ω ^ ω ^ b ≤ ω ^ ω ^ b

Tactic:
ax,

Goal state after:
case inr.a
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
x : Ordinal.{u}
xb : x < ω ^ b
ax : a < ω ^ x
⊢ ω ^ x * ω ^ ω ^ b ≤ ω ^ ω ^ b
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
⊢ a * b ≤ b ^ succ (log b a)

Tactic:
rw [(isNormal_mul_right (pos_iff_ne_zero.2 ha)).apply_of_isSuccLimit hbl,
      Ordinal.iSup_le_iff]

Goal state after:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
⊢ ∀ (i : ↑(Set.Iio b)), a * ↑i ≤ b ^ succ (log b a)
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
⊢ (a ^ b).card ≤ max a.card b.card

Tactic:
by
  induction b using limitRecOn with
  | zero => simpa using one_lt_omega0.le.trans ha
  | add_one b IH =>
    rw [opow_add_one, card_mul, card_add_one, Cardinal.mul_eq_max_of_aleph0_le_right, max_comm]
    · grw [IH]
      rw [← max_assoc, max_self]
      grw [← le_self_add]
    · rw [ne_eq, card_eq_zero, opow_eq_zero]
      rintro ⟨rfl, -⟩
      cases omega0_pos.not_ge ha
    · rwa [aleph0_le_card]
  | limit b hb IH =>
    rw [(isNormal_opow (one_lt_omega0.trans_le ha)).apply_of_isSuccLimit hb]
    exact card_iSup_Iio_le (le_max_right ..) fun i ↦
      (IH i i.2).trans (max_le_max_left _ (card_le_card i.2.le))

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

Goal state before:
pp: o : Ordinal.{u}
⊢ ∃ f, o.cof.ord.blsub f = o

Tactic:
rcases exists_lsub_cof o with ⟨ι, f, hf, hι⟩

Goal state after:
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hι : #ι = o.cof
⊢ ∃ f, o.cof.ord.blsub f = o
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #↑(t i) < c
⊢ #↑(⋃ i, t i) < c

Tactic:
apply lt_of_le_of_lt (Cardinal.mk_sUnion_le _)

Goal state after:
c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #↑(t i) < c
⊢ #↑(range fun i ↦ t i) * ⨆ s, #↑↑s < c
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} #(α ≃ α) = lift.{u, max u v} #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = lift.{u, max u v} #(α → β')
⊢ #(α ≃ β') = #(α → β')

Tactic:
rw [lift_id'.{u, v}] at e₁ e₂

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_1
inst✝ : Infinite α
s : Set α
h2 : #↑s < #α
⊢ #↑sᶜ = #α

Tactic:
refine eq_of_add_eq_of_aleph0_le ?_ h2 (aleph0_le_mk α)

Goal state after:
α : Type u_1
inst✝ : Infinite α
s : Set α
h2 : #↑s < #α
⊢ #↑s + #↑sᶜ = #α
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case pos
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
h : j ∈ {i}
⊢ (single i (x i)) i = x i

Tactic:
single_eq_same

Goal state after:
case pos
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
h : j ∈ {i}
⊢ x i = x i
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
f : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
⊢ p f

Tactic:
obtain ⟨f, s⟩ := f

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
f : (i : ι) → β i
s : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ p { toFun := f, support' := s }
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case h.empty
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
f : (i : ι) → β i
H : ∀ (i : ι), i ∈ 0 ∨ f i = 0
⊢ p { toFun := f, support' := Trunc.mk ⟨0, H⟩ }

Tactic:
have : f = 0 := funext fun i => (H i).resolve_left (Multiset.notMem_zero _)
    subst this
    exact h0

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

Goal state before:
pp: case inl
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ ⟨i, j⟩.fst ⟨i, j⟩.snd
j' : α i
⊢ (single ⟨i, j⟩ x) ⟨i, j'⟩ = ((single i (single j x)) i) j'

Tactic:
single_eq_same

Goal state after:
case inl
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ ⟨i, j⟩.fst ⟨i, j⟩.snd
j' : α i
⊢ (single ⟨i, j⟩ x) ⟨i, j'⟩ = (single j x) j'
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: case inl.inl
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j' : α i
x : δ ⟨i, j'⟩.fst ⟨i, j'⟩.snd
⊢ x = (single j' x) j'

Tactic:
single_eq_same

Goal state after:
case inl.inl
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j' : α i
x : δ ⟨i, j'⟩.fst ⟨i, j'⟩.snd
⊢ x = x
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
i : ι
⊢ i ∈ f.support ↔ f i ≠ 0

Tactic:
obtain ⟨f, s⟩ := f

Goal state after:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : (i : ι) → β i
s : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ i ∈ { toFun := f, support' := s }.support ↔ { toFun := f, support' := s } i ≠ 0
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: case inl
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → (j : α i) → Zero (δ i j)
inst✝ : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
j' : α i
⊢ ((single i (single j x)) i) j' = (single ⟨i, j⟩ x) ⟨i, j'⟩

Tactic:
single_eq_same

Goal state after:
case inl
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → (j : α i) → Zero (δ i j)
inst✝ : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
j' : α i
⊢ (single j x) j' = (single ⟨i, j⟩ x) ⟨i, j'⟩
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: case inl.inl
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → (j : α i) → Zero (δ i j)
inst✝ : (i : ι) → DecidableEq (α i)
i : ι
j' : α i
x : δ i j'
⊢ x = (single ⟨i, j'⟩ x) ⟨i, j'⟩

Tactic:
single_eq_same

Goal state after:
case inl.inl
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → (j : α i) → Zero (δ i j)
inst✝ : (i : ι) → DecidableEq (α i)
i : ι
j' : α i
x : δ i j'
⊢ x = x
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
f_eq : ∏ i ∈ f.support ∪ g.support, h i (f i) = f.prod h
g_eq : ∏ i ∈ f.support ∪ g.support, h i (g i) = g.prod h
⊢ f.prod h * ∏ i ∈ f.support ∪ g.support, h i (g i) = f.prod h * g.prod h

Tactic:
g_eq

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
f_eq : ∏ i ∈ f.support ∪ g.support, h i (f i) = f.prod h
g_eq : ∏ i ∈ f.support ∪ g.support, h i (g i) = g.prod h
⊢ f.prod h * g.prod h = f.prod h * g.prod h
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
⊢ ∑ i ∈ sx.toFinset, (φ i) (f i) = ∑ i ∈ sy.toFinset, (φ i) (f i)

Tactic:
have H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset := Finset.inter_subset_right

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
⊢ ∑ i ∈ sx.toFinset, (φ i) (f i) = ∑ i ∈ sy.toFinset, (φ i) (f i)
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: case refine_1
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
⊢ ∀ x ∈ sx.toFinset, x ∉ sx.toFinset ∩ sy.toFinset → (φ x) (f x) = 0

pp: case refine_2
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
⊢ ∀ x ∈ sx.toFinset ∩ sy.toFinset, (φ x) (f x) = (φ x) (f x)

pp: case refine_3
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
⊢ ∀ x ∈ sy.toFinset, x ∉ sx.toFinset ∩ sy.toFinset → (φ x) (f x) = 0

Tactic:
· intro i H1 H2
        rw [Finset.mem_inter] at H2
        simp only [Multiset.mem_toFinset] at H1 H2
        convert! map_zero (φ i)
        exact (hy i).resolve_left (mt (And.intro H1) H2)

Goal state after:
case refine_2
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
⊢ ∀ x ∈ sx.toFinset ∩ sy.toFinset, (φ x) (f x) = (φ x) (f x)

case refine_3
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
⊢ ∀ x ∈ sy.toFinset, x ∉ sx.toFinset ∩ sy.toFinset → (φ x) (f x) = 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case inl
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
i : κ
x : β (h i)
⊢ x = (single i x) i

Tactic:
single_eq_same

Goal state after:
case inl
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
i : κ
x : β (h i)
⊢ x = x
Module: Mathlib.Data.DFinsupp.Defs

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

Tactic:
single_eq_same

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

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

Tactic:
single_eq_same

Goal state after:
case none
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
x : α none
⊢ x = x
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 = f (r • 1)

Tactic:
rw [map_smul, smul_eq_mul, mul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ f.dualMap.ker = (Dual.eval R M' ∘ₗ f).range.dualCoannihilator

Tactic:
ext x; simp [LinearMap.ext_iff (f := dualMap f x)]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
⊢ AddMonoidHom.mrange (mapRange.addMonoidHom f) =
    AddSubmonoid.comap coeFnAddMonoidHom (AddSubmonoid.pi Set.univ fun i ↦ AddMonoidHom.mrange (f i))

Tactic:
classical
  ext x
  simp only [AddSubmonoid.mem_comap, coeFnAddMonoidHom_apply]
  refine ⟨fun ⟨y, hy⟩ i hi ↦ ?_, fun h ↦ ?_⟩
  · simp [← hy]
  · choose g hg using fun i => h i (Set.mem_univ _)
    use DFinsupp.mk x.support (g ·)
    ext i
    simp only [Finset.coe_sort_coe, mapRange.addMonoidHom_apply, mapRange_apply]
    by_cases mem : i ∈ x.support
    · rw [mk_of_mem mem, hg]
    · rw [DFinsupp.notMem_support_iff.mp mem, mk_of_notMem mem, map_zero]

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

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : ↑t ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : g i • f i + g j • f j = 0
ht' : t ⊆ {i, j}
⊢ ∀ i ∈ t, g i = 0

Tactic:
obtain ⟨hi0, hj0⟩ := h _ _ h0

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : ↑t ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : g i • f i + g j • f j = 0
ht' : t ⊆ {i, j}
hi0 : g i = 0
hj0 : g j = 0
⊢ ∀ i ∈ t, g 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
⊢ ∑ x ∈ s.erase i, v x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j

Tactic:
exact SetLike.le_def.mp (biSup_mono <| by grind) (Submodule.sum_mem_biSup <| by grind)

Goal state after: