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

Goal state before:
pp: R : Type u_4
A : Type u_5
M : Type u_6
inst✝⁶ : Semiring A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module A M
inst✝³ : CommSemiring R
inst✝² : Algebra R A
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
h : Surjective ⇑(algebraMap R A)
s : Finset M
⊢ (restrictScalars R (span A ↑s)).FG

Tactic:
exact ⟨s, .symm <| restrictScalars_span R A h _⟩

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
hM' : M'.FG
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
⊢ ∃ n, M' = N n

Tactic:
by
  obtain ⟨S, hS⟩ := hM'
  have (s : S) : ∃ n, (s : M) ∈ N n :=
    (mem_iSup_of_chain N s).mp (by simpa [H, ← hS] using subset_span s.prop)
  choose f hf using this
  use S.attach.sup f
  apply le_antisymm
  · rw [← hS, span_le]
    intro s hs
    exact N.monotone' (Finset.le_sup <| S.mem_attach ⟨s, hs⟩) (hf _)
  · rw [← H]
    exact le_iSup ..

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
_b : β
hb : 0 ≤ _b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ 0 ≤ a₂ • _b - a₁ • _b

Tactic:
← sub_smul

Goal state after:
α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
_b : β
hb : 0 ≤ _b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ 0 ≤ (a₂ - a₁) • _b
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
_b : β
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
⊢ 0 < a₂ • _b - a₁ • _b

Tactic:
← sub_smul

Goal state after:
α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
_b : β
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
⊢ 0 < (a₂ - a₁) • _b
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✝¹ : Zero γ
inst✝ : SMulPosReflectLE α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 < b
a₁ a₂ : α
h : a₁ • b ≤ a₂ • b
⊢ a₁ ≤ a₂

Tactic:
simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosReflectLE α γ
b : β
a₁ a₂ : α
hf : ∀ {b₁ b₂ : β}, True
smul : ∀ (a : α) (b : β), True
zero : True
hb : 0 < f b
h : a₁ • f b ≤ a₂ • f b
⊢ a₁ ≤ a₂
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✝¹ : Zero γ
inst✝ : SMulPosReflectLT α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
⊢ a₁ < a₂

Tactic:
simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosReflectLT α γ
b : β
a₁ a₂ : α
hf : ∀ {b₁ b₂ : β}, True
smul : ∀ (a : α) (b : β), True
zero : True
hb : 0 ≤ f b
h : a₁ • f b < a₂ • f b
⊢ a₁ < a₂
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: α : Type u
⊢ Small.{v, u} α ↔ lift.{v + 1, u} #α < univ.{v, max u (v + 1)}

Tactic:
rw [lt_univ']

Goal state after:
α : Type u
⊢ Small.{v, u} α ↔ ∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'
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:
rwa [← @Sum.lex_inr_inr _ t _ s, ← hg, ← hg, f.map_rel_iff, Sum.lex_inr_inr]

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

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_3} ι
i : ι
⊢ f i + 1 ≤ ⨆ i, f i + 1

Tactic:
apply Ordinal.le_iSup

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

Goal state before:
pp: o : Ordinal.{u}
⊢ (typein LT.lt).toRelEmbedding o = lift.{u + 1, u} (typeLT o.ToType)

Tactic:
← ToType.mk.toRelIsoLT.ordinal_lift_type_eq,

Goal state after:
o : Ordinal.{u}
⊢ (typein LT.lt).toRelEmbedding o = lift.{u, u + 1} (typeLT ↑(Iio o))
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u_1}
⊢ a ≤ b → ∃ c, b = a + c

Tactic:
refine inductionOn₂ a b fun α r _ β s _ ⟨f⟩ ↦ ?_
    obtain ⟨γ, t, _, ⟨g⟩⟩ := f.exists_sum_relIso
    exact ⟨type t, g.ordinalType_congr.symm⟩

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

Goal state before:
pp: case pos
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : BddAbove (range f)
i : β
⊢ f i + 1 ≤ ⨆ i, f i

Tactic:
obtain ⟨j, hj⟩ := exists_gt i

Goal state after:
case pos
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : BddAbove (range f)
i j : β
hj : i < j
⊢ f i + 1 ≤ ⨆ i, f i
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal.{u}
ho : type r = o
ho' : type r' = o
f : (a : Ordinal.{u}) → a < o → Ordinal.{u_3}
⊢ range (familyOfBFamily' r ho f) = range (familyOfBFamily' r' ho' f)

Tactic:
range_familyOfBFamily'

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

Goal state before:
pp: a b c : Ordinal.{u_4}
ba : b + a = a
⊢ (a + b) * (c + 1) = a * (c + 1) + b

Tactic:
induction c using limitRecOn with
  | zero => simp
  | add_one c IH => rw [mul_add_one, IH, ← add_assoc, add_assoc _ b, ba, ← mul_add_one]
  | limit c l IH => rw [mul_add_one, add_mul_limit_aux ba l IH, mul_add_one, add_assoc]

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

Goal state before:
pp: case inr
b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
H₁ : b ^ (log.go y b y).snd ≤ y
H₂ : y < b ^ ((log.go y b y).snd + 1)
h : (log.go y b y).snd ≥ x
⊢ (log.go y b y).snd < x ↔ y < b ^ x

Tactic:
| inr h =>

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ (#↑s).ord < type r

Tactic:
grw [← ord_le_type, ord_lt_ord, ← mk_univ (α := α)]
  exact card_lt_card_of_left_finite hfin h.ssubset_univ

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

Goal state before:
pp: case refine_1
a b : Ordinal.{u_1}
⊢ 1 < a ^ b → 1 < a ∧ b ≠ 0

pp: case refine_2
a b : Ordinal.{u_1}
x✝ : 1 < a ∧ b ≠ 0
ha : 1 < a
hb : b ≠ 0
⊢ 1 < a ^ b

Tactic:
· contrapose! +distrib
    rw [le_one_iff]
    rintro ((rfl | rfl) | rfl)
    · exact zero_opow_le b
    · simp
    · simp

Goal state after:
case refine_2
a b : Ordinal.{u_1}
x✝ : 1 < a ∧ b ≠ 0
ha : 1 < a
hb : b ≠ 0
⊢ 1 < a ^ b
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case inr
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
⊢ o * sSup s = sSup ((fun x ↦ o * x) '' s)

Tactic:
rcases eq_zero_or_pos o with (rfl | ho)

Goal state after:
case inr.inl
s : Set Ordinal.{u_1}
hs : s.Nonempty
⊢ 0 * sSup s = sSup ((fun x ↦ 0 * x) '' s)

case inr.inr
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
⊢ o * sSup s = sSup ((fun x ↦ o * x) '' s)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case hbc
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ b ^ u * (v + 1) ≤ b ^ u * x

Tactic:
add_one_le_of_lt hv

Goal state after:
case hbc
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ b ^ u * x ≤ b ^ u * x
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: x : Ordinal.{u_1}
⊢ x ∈ range ⇑ω_ ↔ ω ≤ x ∧ x.IsInitial

Tactic:
rw [range_omega, mem_ofPred]

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

Goal state before:
pp: o : Ordinal.{u_1}
ho : ω ^ 2 ≤ o
⊢ preOmega o = ω_ o

Tactic:
rw [← opow_natCast] at ho
  rw [omega_eq_preOmega, add_of_omega0_opow_le _ ho]
  apply left_lt_opow one_lt_omega0
  simp

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ preAleph 0 < preAleph o ↔ 0 < o

Tactic:
preAleph_lt_preAleph

Goal state after:
o : Ordinal.{u_1}
⊢ 0 < o ↔ 0 < o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
this : a ^ ω * b + c ≤ a ^ ω * d
⊢ succ b ≤ d

Tactic:
have := (add_lt_add_right hc (a ^ ω * b)).trans_le this

Goal state after:
case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
this✝ : a ^ ω * b + c ≤ a ^ ω * d
this : a ^ ω * b + 0 < a ^ ω * d
⊢ succ b ≤ d
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_2
a : Ordinal.{u}
ha : 0 < a
c : Ordinal.{u}
h : deriv (fun x ↦ a * x) c = a ^ ω * c
⊢ nfp (fun x ↦ a * x) (succ (a ^ ω * c)) = a ^ ω * succ c

Tactic:
exact nfp_mul_opow_omega0_add c ha zero_lt_one (one_le_iff_pos.2 (opow_pos _ ha))

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

Goal state before:
pp: b o : Ordinal.{u}
hb : 1 < b
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) (b ^ o)
x y : Ordinal.{u}
hx : x < o
hy : y < o
this : b ^ x * b ^ y < b ^ o
⊢ x + y < o

Tactic:
rwa [← opow_add, opow_lt_opow_iff_right hb] at this

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

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

Tactic:
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.Ordinal.FundamentalSequence

Goal state before:
pp: case a
a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
b : Ordinal.{u_1}
hb : b < o
c : ↑(Iio a)
hc : b ≤ ↑(f c)
⊢ ↑(f c) + 1 ≤ ⨆ i, ↑(f i) + 1

Tactic:
apply Ordinal.le_iSup

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
⊢ range v ⊆ range v'

Tactic:
rintro - ⟨k, rfl⟩

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
k : κ
⊢ v k ∈ range v'
Module: Mathlib.SetTheory.Cardinal.Regular

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

Tactic:
induction a using limitRecOn with
  | zero =>
    rw [derivFamily_zero]
    exact nfpFamily_lt_ord_lift hω (by rwa [hc.cof_ord]) hf
  | add_one b hb =>
    intro hb'
    rw [derivFamily_add_one]
    exact
      nfpFamily_lt_ord_lift hω (by rwa [hc.cof_ord]) hf
        ((isSuccLimit_ord hc.1).succ_lt (hb ((lt_succ b).trans hb')))
  | limit b hb H =>
    intro hb'
    rw [derivFamily_limit f hb]
    apply Ordinal.lift_iSup_lt_of_lt_cof
    · rwa [← lift_cof, hc.cof_ord, mk_Iio_ordinal, lift_lift, lift_lt, ← lt_ord]
    · exact fun i ↦ H i.1 i.2 <| i.2.trans hb'

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

Goal state before:
pp: o : Ordinal.{u_1}
hc : IsSuccLimit o ∧ o.cof < ℵ_ o
⊢ ℵ_ ω ≤ ℵ_ o

Tactic:
rw [aleph_le_aleph]

Goal state after:
o : Ordinal.{u_1}
hc : IsSuccLimit o ∧ o.cof < ℵ_ o
⊢ ω ≤ o
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
⊢ ∀ (i : ↑(Iio a)), 2 ^ preBeth ↑i < c

Tactic:
rintro ⟨b, hb⟩
    exact hc.isStrongPrelimit <| IH _ hb (hb.trans ha)

Goal state after:
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
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
i : ι
⊢ i ∈ ↑xs + ↑ys ∨ f i (x i) (y i) = 0

Tactic:
obtain h1 | (h1 : x i = 0) := xs.prop i

Goal state after:
case inl
ι : 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
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
i : ι
h1 : i ∈ ↑xs
⊢ i ∈ ↑xs + ↑ys ∨ f i (x i) (y i) = 0

case inr
ι : 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
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
i : ι
h1 : x i = 0
⊢ i ∈ ↑xs + ↑ys ∨ f i (x i) (y i) = 0
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✝
a : (i : ι) → α i
⊢ Quotient.map (fun a i ↦ a i ⋯) ⋯ (listChoice fun i x ↦ ⟦a i⟧) =
    Quotient.map (fun a i ↦ a i ⋯) ⋯ (listChoice fun i x ↦ ⟦a i⟧)

Tactic:
listChoice_mk,

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 ⋯) ⋯ ⟦fun x1 x2 ↦ a x1⟧ = Quotient.map (fun a i ↦ a i ⋯) ⋯ ⟦fun x1 x2 ↦ a x1⟧
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
i : ι
a✝ : i ∈ Finset.univ
hi : i ∉ v.support
⊢ f i (v i) = 1

Tactic:
rw [mem_support_iff, not_not] at hi

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
i : ι
a✝ : i ∈ Finset.univ
hi : v i = 0
⊢ f i (v i) = 1
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: case mk.mk.e_a
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
f : (i : ι) → β i
support'✝¹ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
⊢ ∑ x ∈ (sf + sg).toFinset, (φ x) (f x) = ∑ x ∈ sf.toFinset, (φ x) (f x)

Tactic:
refine (Finset.sum_subset ?_ ?_).symm
      · intro i
        simp only [Multiset.mem_toFinset, Multiset.mem_add]
        exact Or.inl
      · intro i _ H2
        simp only [Multiset.mem_toFinset] at H2
        rw [(hf i).resolve_left H2, map_zero]

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

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
f : Dual R M
g : Dual R (Dual R M)
⊢ f ((evalEquiv R M).symm g) = g f

Tactic:
set m := (evalEquiv R M).symm g

Goal state after:
R : Type u_3
M : Type u_4
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
f : Dual R M
g : Dual R (Dual R M)
m : M := (evalEquiv R M).symm g
⊢ f m = g f
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
inj : Injective ⇑f
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ j, ⨆ (_ : j ≠ i), m j ≤ ⊥
⊢ ∀ (i : ι), map f (m i) ⊓ ⨆ j, ⨆ (_ : j ≠ i), map f (m j) ≤ ⊥

Tactic:
rintro i _ ⟨⟨x, hxi, rfl⟩, hx⟩

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
inj : Injective ⇑f
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ j, ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ ↑(m i)
hx : f x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), map f (m j))
⊢ f x ∈ ⊥
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case inl
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
indep : Set ι → Prop := fun s ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I // indep I }
r : X → X → Prop := fun I J ↦ ↑I ⊆ ↑J
f g : ι →₀ R
hsum : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
hc : IsChain r ∅
hfsupp : f ∈ Finsupp.supported R R (⋃ I ∈ ∅, ↑I)
hgsupp : g ∈ Finsupp.supported R R (⋃ I ∈ ∅, ↑I)
⊢ 0 = g

Tactic:
show g = 0 by simpa using! hgsupp

Goal state after:
case inl
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
indep : Set ι → Prop := fun s ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I // indep I }
r : X → X → Prop := fun I J ↦ ↑I ⊆ ↑J
f g : ι →₀ R
hsum : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
hc : IsChain r ∅
hfsupp : f ∈ Finsupp.supported R R (⋃ I ∈ ∅, ↑I)
hgsupp : g ∈ Finsupp.supported R R (⋃ I ∈ ∅, ↑I)
⊢ 0 = 0
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
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
this : (a * d) • s = (b * c) • s
⊢ s = 0

Tactic:
by_contra hs

Goal state after:
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
this : (a * d) • s = (b * c) • s
hs : ¬s = 0
⊢ False
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ x ∈ a.support ↔ (coeff x) a ≠ 0

Tactic:
by
  rw [support, Finsupp.mem_support_iff]
  exact Iff.rfl

Goal state after:
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
a : FreeAbelianGroup X
⊢ a.support.Nonempty ↔ a ≠ 0

Tactic:
contrapose!; exact support_eq_empty

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
s : Set ι
a : ι
f : ι → V
has : a ∉ s
⊢ LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ f a ∉ span K (f '' s)

Tactic:
classical
  rw [LinearIndepOn, LinearIndepOn, ← linearIndependent_equiv
    ((Equiv.optionEquivSumPUnit _).trans (Equiv.Set.insert has).symm), linearIndependent_option]
  simp only [comp_def]
  rw [range_comp']
  simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
⊢ (mapDomainRingHom R ↑e).comp (mapDomainRingHom R ↑e.symm) = RingHom.id R[N]

Tactic:
apply MonoidAlgebra.ringHom_ext

Goal state after:
case h₁
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
⊢ ∀ (r : R), ((mapDomainRingHom R ↑e).comp (mapDomainRingHom R ↑e.symm)) (single 1 r) = (RingHom.id R[N]) (single 1 r)

case h_of
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
⊢ ∀ (m : N), ((mapDomainRingHom R ↑e).comp (mapDomainRingHom R ↑e.symm)) (single m 1) = (RingHom.id R[N]) (single m 1)