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

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

Tactic:
rcases Cardinal.exists_ord_eq ι with ⟨r, hr, hι'⟩
      rw [← @blsub_eq_lsub' ι r hr] at hf
      simpa using H _ hf

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

Goal state before:
pp: c : Cardinal.{u}
h : ℵ₀ ≤ c
n : ℕ
hn : 2 ≤ n
⊢ 2 ≤ ↑n

Tactic:
assumption_mod_cast

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

Goal state before:
pp: case inl
β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
hα : #α < ℵ₀
⊢ ∃ a, succ #α ≤ #↑(f ⁻¹' {a})

pp: case inr
β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
hα : ℵ₀ ≤ #α
⊢ ∃ a, succ #α ≤ #↑(f ⁻¹' {a})

Tactic:
· obtain ⟨a, ha⟩ := infinite_pigeonhole_card f ℵ₀ hβ le_rfl
      (by rwa [isRegular_aleph0.cof_ord])
    exact ⟨a, ha.trans' (succ_le_of_lt hα)⟩

Goal state after:
case inr
β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
hα : ℵ₀ ≤ #α
⊢ ∃ a, succ #α ≤ #↑(f ⁻¹' {a})
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = Set.univ
h : #↑(range f) < #β
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b ↦
    Eq.mp (Eq.trans mem_iUnion._simp_1 (congrArg Exists (funext fun i ↦ SetLike.mem_coe._simp_1)))
      (Eq.ge w (mem_univ b))
⊢ False

Tactic:
let u' : β → range f := fun b => ⟨f (u b).choose, by simp⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = Set.univ
h : #↑(range f) < #β
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b ↦
    Eq.mp (Eq.trans mem_iUnion._simp_1 (congrArg Exists (funext fun i ↦ SetLike.mem_coe._simp_1)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) := fun b ↦ ⟨f ⋯.choose, ⋯⟩
⊢ False
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i i' : ι
b : β i
⊢ (single i b) i' = if h : i = i' then Eq.recOn h b else 0

Tactic:
rw [single_eq_pi_single, Pi.single, Function.update]

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i i' : ι
b : β i
⊢ (if h : i' = i then ⋯ ▸ b else 0 i') = if h : i = i' then Eq.recOn h b else 0
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: ι : 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
i' : ι
j' : α i'
⊢ (single ⟨i, j⟩ x) ⟨i', j'⟩ = ((single i (single j x)) i') j'

Tactic:
obtain rfl | hi := eq_or_ne i i'

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 i (single j x)) i) j'

case inr
ι : 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
i' : ι
j' : α i'
hi : i ≠ i'
⊢ (single ⟨i, j⟩ x) ⟨i', j'⟩ = ((single i (single j x)) i') j'
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: ι : 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
i' : ι
j' : α i'
⊢ ((single i (single j x)) i') j' = (single ⟨i, j⟩ x) ⟨i', j'⟩

Tactic:
obtain rfl | hi := eq_or_ne i i'

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 i (single j x)) i) j' = (single ⟨i, j⟩ x) ⟨i, j'⟩

case inr
ι : 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
i' : ι
j' : α i'
hi : i ≠ i'
⊢ ((single i (single j x)) i') j' = (single ⟨i, j⟩ x) ⟨i', j'⟩
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: case neg
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : ¬b ≠ 0
⊢ (single i b).prod h✝ = h✝ i b

Tactic:
not_not

Goal state after:
case neg
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : b = 0
⊢ (single i b).prod h✝ = h✝ i b
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case inl
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
h : b ≠ 0
⊢ i ∈ (f.update i b).support ↔ i ∈ insert i f.support

pp: case inr
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
h : b ≠ 0
j : ι
hi : i ≠ j
⊢ j ∈ (f.update i b).support ↔ j ∈ insert i f.support

Tactic:
· simp [h]

Goal state after:
case inr
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
h : b ≠ 0
j : ι
hi : i ≠ j
⊢ j ∈ (f.update i b).support ↔ j ∈ insert i f.support
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 : ¬v i ≠ 0
⊢ f i (v i) = 1

Tactic:
not_not

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.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → DecidableEq (β i)
f g : Π₀ (i : ι), β i
x✝ : f.support = g.support ∧ ∀ i ∈ f.support, f i = g i
h₁ : f.support = g.support
h₂ : ∀ i ∈ f.support, f i = g i
i : ι
h : ¬f i ≠ 0
⊢ f i = 0

Tactic:
not_not

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → DecidableEq (β i)
f g : Π₀ (i : ι), β i
x✝ : f.support = g.support ∧ ∀ i ∈ f.support, f i = g i
h₁ : f.support = g.support
h₂ : ∀ i ∈ f.support, f i = g i
i : ι
h : f i = 0
⊢ f i = 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → DecidableEq (β i)
f g : Π₀ (i : ι), β i
x✝ : f.support = g.support ∧ ∀ i ∈ f.support, f i = g i
h₁ : f.support = g.support
h₂ : ∀ i ∈ f.support, f i = g i
i : ι
h : ¬g i ≠ 0
hf : f i = 0
⊢ g i = 0

Tactic:
not_not

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → DecidableEq (β i)
f g : Π₀ (i : ι), β i
x✝ : f.support = g.support ∧ ∀ i ∈ f.support, f i = g i
h₁ : f.support = g.support
h₂ : ∀ i ∈ f.support, f i = g i
i : ι
h : g i = 0
hf : f i = 0
⊢ g i = 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
i✝ : κ
⊢ (comapDomain h hh 0) i✝ = 0 i✝

Tactic:
zero_apply,

Goal state after:
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
i✝ : κ
⊢ (comapDomain h hh 0) i✝ = 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
i✝ : κ
⊢ (comapDomain' h hh' 0) i✝ = 0 i✝

Tactic:
zero_apply,

Goal state after:
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
i✝ : κ
⊢ (comapDomain' h hh' 0) i✝ = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
⊢ ⨆ i, ⨆ (_ : p i), S i ≤ (((lsum ℕ) fun i ↦ (S i).subtype) ∘ₗ filterLinearMap R (fun i ↦ ↥(S i)) p).range

Tactic:
refine iSup₂_le fun i hi y hy => ⟨DFinsupp.single i ⟨y, hy⟩, ?_⟩
    rw [LinearMap.comp_apply, filterLinearMap_apply, filter_single_pos _ _ hi]
    simp only [lsum_apply_apply, sumAddHom_single, LinearMap.toAddMonoidHom_coe, coe_subtype]

Goal state after:
Module: Mathlib.Algebra.Algebra.Opposite

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra S A
inst✝¹ : SMulCommClass R S A
inst✝ : IsScalarTower R S A
x✝ : R
⊢ (RingEquiv.moduleEndSelf A).toFun ((algebraMap R Aᵐᵒᵖ) x✝) = (algebraMap R (Module.End A A)) x✝

Tactic:
by ext; simp [Algebra.algebraMap_eq_smul_one]

Goal state after:
Module: Mathlib.Algebra.Algebra.Opposite

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra S A
inst✝¹ : SMulCommClass R S A
inst✝ : IsScalarTower R S A
x✝ : R
⊢ (RingEquiv.moduleEndSelfOp A).toFun ((algebraMap R A) x✝) = (algebraMap R (Module.End Aᵐᵒᵖ A)) x✝

Tactic:
by ext; simp [Algebra.algebraMap_eq_smul_one]

Goal state after:
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
N : Type u_6
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : span R (Set.range v) = ⊤
hli : LinearIndependent R (⇑f ∘ v)
hsp : span R (Set.range (⇑f ∘ v)) = ⊤
⊢ Surjective ⇑f

Tactic:
Set.range_comp,

Goal state after:
R : Type u_2
M : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_6
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : span R (Set.range v) = ⊤
hli : LinearIndependent R (⇑f ∘ v)
hsp : span R (⇑f '' Set.range v) = ⊤
⊢ Surjective ⇑f
Module: Mathlib.Algebra.Group.AddChar

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

Tactic:
Finset.prod_apply

Goal state after:
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
s : Finset ι
ψ : ι → AddChar A M
a : A
⊢ ∏ c ∈ s, (ψ c) a = ∏ i ∈ s, (ψ i) a
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: case pos
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : Decidable (ψ = 0)
h : ψ = 0
⊢ ∑ a, ψ a = ↑(card A)

pp: case neg
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : Decidable (ψ = 0)
h : ¬ψ = 0
⊢ ∑ a, ψ a = 0

Tactic:
· simp [h]

Goal state after:
case neg
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : Decidable (ψ = 0)
h : ¬ψ = 0
⊢ ∑ a, ψ a = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
n : ℕ
v : Fin n → V
⊢ LinearIndependent K (Fin.cons x v ∘ ⇑(finRotate (n + 1))) ↔ LinearIndependent K v ∧ x ∉ span K (range v)

Tactic:
linearIndependent_equiv,

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
n : ℕ
v : Fin n → V
⊢ LinearIndependent K (Fin.cons x v) ↔ LinearIndependent K v ∧ x ∉ span K (range v)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
n : ℕ
v : Fin (n + 1) → V
⊢ LinearIndependent K v ↔ LinearIndependent K (Fin.init v) ∧ v (Fin.last n) ∉ span K (range (Fin.init v))

Tactic:
by
  rw [← linearIndependent_finSnoc, Fin.snoc_init_self]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
δ : Type u_7
δ' : Type u_8
ε : Type u_9
inst✝² : DecidableEq δ'
inst✝¹ : DecidableEq ε
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
γ : Type u_14
u : Finset γ
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ ↑(image₂ f s (image₂ g t u)) = ↑(image₂ g' t (image₂ f' s u))

Tactic:
by
    push_cast
    exact image2_left_comm h_left_comm

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

Goal state before:
pp: 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✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this✝ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ ↑(span K ↑(s' ∪ t))
hb₂t' : b₂ ∉ s' ∪ t
this : s ⊆ ↑(span K ↑(insert b₂ s' ∪ t))
⊢ ↑(insert b₂ s') ⊆ s

Tactic:
by simp [insert_subset_iff, hb₂s, hs']

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝¹ : SemilatticeSup δ
inst✝ : OrderBot δ
g : γ → δ
⊢ (image₂ f s t).sup g = t.sup fun y ↦ s.sup fun x ↦ g (f x y)

Tactic:
simp only [image₂, sup_image, sup_product_right]

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝¹ : SemilatticeSup δ
inst✝ : OrderBot δ
g : γ → δ
⊢ (t.sup fun i' ↦ s.sup fun i ↦ (g ∘ uncurry f) (i, i')) = t.sup fun y ↦ s.sup fun x ↦ g (f x y)
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ⇑f
h : UniqueMul A B a0 b0
x✝¹ x✝ : H
⊢ x✝¹ ∈ image (⇑f) A → x✝ ∈ image (⇑f) B → x✝¹ * x✝ = f a0 * f b0 → x✝¹ = f a0 ∧ x✝ = f b0

Tactic:
by
    simp_rw [Finset.mem_image]
    rintro ⟨a, aA, rfl⟩ ⟨b, bB, rfl⟩ ab
    simp_rw [← map_mul, hf.eq_iff] at ab ⊢
    exact h aA bB ab

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0

Tactic:
contrapose! +distrib
    rintro (hs | rfl)
    · exact hs.pow
    · simp

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

Goal state before:
pp: case convert_7
n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
⊢ k = n

Tactic:
simp [← h, card_compl]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
u : (Finset α)ˣ
⊢ ∃ a, ↑u = {a} ∧ IsUnit a

Tactic:
obtain ⟨a, b, ha, hb, h⟩ := Finset.mul_eq_one_iff.1 u.mul_inv

Goal state after:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
u : (Finset α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ ∃ a, ↑u = {a} ∧ IsUnit a
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
u : (Finset α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ {b * a} = {1}

Tactic:
rw [← singleton_mul_singleton, ← ha, ← hb]

Goal state after:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
u : (Finset α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ ↑u⁻¹ * ↑u = {1}
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
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
let C := A.map ⟨_, mul_right_injective a⁻¹⟩

Goal state after:
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
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
r : R
⊢ X * (monomial n) r = (monomial (n + 1)) r

Tactic:
by
  rw [X_mul, monomial_mul_X]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : IsDomain R
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
⊢ LinearIndependent R ((fun i ↦ single i (v i)) ∘ ⇑(Equiv.sigmaPUnit ι))

Tactic:
exact linearIndependent_single (f := fun i (_ : Unit) ↦ v i) <| by simp +contextual [hv]

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

Goal state before:
pp: M : Type u_3
inst✝ : AddCommMonoid M
S : AddSubmonoid M
⊢ (toNatSubmodule S).FG ↔ ∃ n f, AddMonoidHom.mrange f = (toNatSubmodule S).toAddSubmonoid

Tactic:
Submodule.fg_iff_exists_fin_linearMap

Goal state after:
M : Type u_3
inst✝ : AddCommMonoid M
S : AddSubmonoid M
⊢ (∃ n f, f.range = toNatSubmodule S) ↔ ∃ n f, AddMonoidHom.mrange f = (toNatSubmodule S).toAddSubmonoid
Module: Mathlib.RingTheory.Finiteness.Cardinality

Goal state before:
pp: M : Type u_3
inst✝ : AddCommGroup M
H : AddSubgroup M
⊢ (toIntSubmodule H).FG ↔ ∃ n f, f.range = (toIntSubmodule H).toAddSubgroup

Tactic:
Submodule.fg_iff_exists_fin_linearMap

Goal state after:
M : Type u_3
inst✝ : AddCommGroup M
H : AddSubgroup M
⊢ (∃ n f, f.range = toIntSubmodule H) ↔ ∃ n f, f.range = (toIntSubmodule H).toAddSubgroup
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝² : DecidableEq R
this✝¹ : DecidableEq M
this✝ : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
this : ∀ y ∈ t1, ∃ x ∈ s, f x = y
⊢ ∃ g, ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y

Tactic:
choose g hg1 hg2 using this

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : (y : P) → y ∈ t1 → M
hg1 : ∀ (y : P) (a : y ∈ t1), g y a ∈ s
hg2 : ∀ (y : P) (a : y ∈ t1), f (g y a) = y
⊢ ∃ g, ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
⊢ ((p.prodEquivOfIsCompl q h).symm x).1 = 0 ↔ ↑((p.prodEquivOfIsCompl q h).symm x).1 ∈ q

Tactic:
mem_right_iff_eq_zero_of_disjoint h.disjoint

Goal state after:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
⊢ ((p.prodEquivOfIsCompl q h).symm x).1 = 0 ↔ ((p.prodEquivOfIsCompl q h).symm x).1 = 0
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case hs2
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf1 : f.ker.FG
hf2 : g.ker.FG
hsur : Surjective ⇑f
⊢ (comap f g.ker ⊓ f.ker).FG

Tactic:
rwa [inf_of_le_right (show (LinearMap.ker f) ≤
      (LinearMap.ker g).comap f from comap_mono bot_le)]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : { f // ∀ (x : ↥p), f ↑x = x }
x : E
⊢ (p.subtype ∘ₗ ↑f * p.subtype ∘ₗ ↑f) x = (p.subtype ∘ₗ ↑f) x

Tactic:
simp [f.2]

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
h : R.dom = ∅
⊢ ∀ (x : α × β), ¬x ∈ R

Tactic:
by simp_all [Set.eq_empty_iff_forall_notMem]

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
h : R.cod = ∅
⊢ ∀ (x : α × β), ¬x ∈ R

Tactic:
by simp_all [Set.eq_empty_iff_forall_notMem]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
x : RelSeries r
⊢ ∀ (i : ℕ) (_hi : i < x.length), (x.toList[i], x.toList[i + 1]) ∈ r

Tactic:
intro i h

Goal state after:
α : Type u_1
r : SetRel α α
x : RelSeries r
i : ℕ
h : i < x.length
⊢ (x.toList[i], x.toList[i + 1]) ∈ r
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case inr.inr
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length + 1) ⟨↑i - (p.length + 1), ⋯⟩
hy : y = Fin.natAdd (p.length + 1) ⟨↑i - p.length, ⋯⟩
⊢ (q.toFun ⟨↑i - (p.length + 1), ⋯⟩, Fin.append p.toFun q.toFun (Fin.natAdd (p.length + 1) ⟨↑i - p.length, ⋯⟩)) ∈ r

Tactic:
Fin.append_right

Goal state after:
case inr.inr
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length + 1) ⟨↑i - (p.length + 1), ⋯⟩
hy : y = Fin.natAdd (p.length + 1) ⟨↑i - p.length, ⋯⟩
⊢ (q.toFun ⟨↑i - (p.length + 1), ⋯⟩, q.toFun ⟨↑i - p.length, ⋯⟩) ∈ r