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

Goal state before:
pp: α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
a : α
x✝ : a ∈ {a | a ≤ sSup S ∧ IsAtom a}
hale : a ≤ sSup S
hatom : IsAtom a
b : α
hbS : b ∈ S
hba : a ≤ b
⊢ a ∈ S

Tactic:
obtain rfl | rfl := (hS b hbS).le_iff.mp hba

Goal state after:
case inl
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
b : α
hbS : b ∈ S
x✝ : ⊥ ∈ {a | a ≤ sSup S ∧ IsAtom a}
hale : ⊥ ≤ sSup S
hatom : IsAtom ⊥
hba : ⊥ ≤ b
⊢ ⊥ ∈ S

case inr
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
a : α
x✝ : a ∈ {a | a ≤ sSup S ∧ IsAtom a}
hale : a ≤ sSup S
hatom : IsAtom a
hbS : a ∈ S
hba : a ≤ a
⊢ a ∈ S
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
M₂ : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
f : M →ₗ[R] M₂
hf : Function.Surjective ⇑f
inst✝ : IsPrincipal R M
⊢ ∃ a, ⊤ = R ∙ a

Tactic:
have ⟨m, hm⟩ := IsPrincipal.principal (⊤ : Submodule R M)

Goal state after:
R : Type u_1
M : Type u_4
M₂ : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
f : M →ₗ[R] M₂
hf : Function.Surjective ⇑f
inst✝ : IsPrincipal R M
m : M
hm : ⊤ = R ∙ m
⊢ ∃ a, ⊤ = R ∙ a
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case hsup
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : s.SupIndep fun i ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb✝ : b ∈ s.biUnion g
hab : b ∉ a
i' : ι'
hi' : i' ∈ s
hb : b ∈ g i'
t : Finset ι' := s.erase i'
u : Finset ι := (g i').erase b
⊢ Disjoint (t.sup fun i ↦ (g i).sup f) ((u ∪ {b}).sup f)

Tactic:
show u ∪ {b} = g i' by grind

Goal state after:
case hsup
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : s.SupIndep fun i ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb✝ : b ∈ s.biUnion g
hab : b ∉ a
i' : ι'
hi' : i' ∈ s
hb : b ∈ g i'
t : Finset ι' := s.erase i'
u : Finset ι := (g i').erase b
⊢ Disjoint (t.sup fun i ↦ (g i).sup f) ((g i').sup f)
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
s : Set α
⊢ IsAtom s → ∃ x, s = {x}

Tactic:
isAtom_iff_le_of_ge,

Goal state after:
α : Type u_2
s : Set α
⊢ (s ≠ ⊥ ∧ ∀ (b : Set α), b ≠ ⊥ → b ⊆ s → s ⊆ b) → ∃ x, s = {x}
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
k : α
⊢ IsCompactElement k ↔ ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x

Tactic:
by
  constructor
  · intro hk s hs hs' h_le
    exact hk s (sSup s) hs hs' (isLUB_sSup s) h_le
  · intro h s u hs hs' hu h_le
    rw [isLUB_iff_sSup_eq] at hu
    rw [← hu] at h_le
    exact h s hs hs' h_le

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = t.sup id}
dir_US : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
sup_S : sSup s ≤ sSup S
⊢ S.Nonempty

Tactic:
suffices ⊥ ∈ S from Set.nonempty_of_mem this

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = t.sup id}
dir_US : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
sup_S : sSup s ≤ sSup S
⊢ ⊥ ∈ S
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedLT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
⊢ {i | t i ≠ ⊥}.Finite

Tactic:
refine Finite.of_finite_image (Finite.subset ?_ (image_subset_range t _)) ht.injOn
  exact WellFoundedLT.finite_of_sSupIndep ht.sSupIndep_range

Goal state after:
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι : Type u_1
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
M : ι → Type u_7
inst✝ : (i : ι) → AddCommMonoid (M i)
p : ((i : ι) → M i) → Prop
f : (i : ι) → M i
zero : p 0
add : ∀ (f g : (i : ι) → M i), p f → p g → p (f + g)
single : ∀ (i : ι) (m : M i), p (Pi.single i m)
val✝ : Fintype ι
⊢ ∀ x ∈ Finset.univ, p (Pi.single x (f x))

Tactic:
simp [single]

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_2.refine_2
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : a ⊓ (b ⊔ sSup s) = ⊥
⊢ a = ⊥

Tactic:
rw [← con, eq_comm, inf_eq_left]

Goal state after:
case refine_2.refine_2
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : a ⊓ (b ⊔ sSup s) = ⊥
⊢ a ≤ b ⊔ sSup s
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ ∏ i ∈ s, g i + ∏ i ∈ s, h i = ∏ i ∈ s, f i

Tactic:
simp_rw [prod_eq_mul_prod_sdiff_singleton_of_mem hi, ← h1, right_distrib]
    congr 2 <;> apply prod_congr rfl <;> simpa

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ comap f (map f p) ≤ p ⊔ f.ker

Tactic:
rintro x ⟨y, hy, e⟩

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
x y : M
hy : y ∈ ↑p
e : f y = f x
⊢ x ∈ p ⊔ f.ker
Module: Mathlib.Data.Finsupp.Ext

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f g : (α →₀ M) →+ N
H : ∀ (x : α) (y : M), f (single x y) = g (single x y)
⊢ Set.EqOn ⇑f ⇑g {f | ∃ a b, f = single a b}

Tactic:
rintro _ ⟨x, y, rfl⟩

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f g : (α →₀ M) →+ N
H : ∀ (x : α) (y : M), f (single x y) = g (single x y)
x : α
y : M
⊢ f (single x y) = g (single x y)
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b₁ b₂ : M
eq : single a b₁ = single a b₂
this : b₁ = (single a b₂) a
⊢ b₁ = b₂

Tactic:
single_eq_same

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b₁ b₂ : M
eq : single a b₁ = single a b₂
this : b₁ = b₂
⊢ b₁ = b₂
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Unique α
b' : M
⊢ b = (single default b') default ↔ b = b'

Tactic:
single_eq_same

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Unique α
b' : M
⊢ b = b' ↔ b = b'
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
x✝ : ∃ b, f = single a b
b : M
hb : f = single a b
⊢ single a b = single a ((single a b) a)

Tactic:
single_eq_same

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
x✝ : ∃ b, f = single a b
b : M
hb : f = single a b
⊢ single a b = single a b
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroOneClass M₀
s t : Set ι
inst✝ : Nontrivial M₀
h : s.indicator 1 = t.indicator 1
⊢ s = t

Tactic:
by
  ext; simp_rw [← indicator_eq_one_iff_mem M₀, h]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case refine_2
α : Type u_1
a : α
⊢ (single a 1) a = 1

pp: α : Type u_1
a : α
⊢ ∀ (b : α), (single a 1) b ≠ 0 → b ≠ a → (single a 1) b = 0

Tactic:
single_eq_same

Goal state after:
case refine_2
α : Type u_1
a : α
⊢ 1 = 1

α : Type u_1
a : α
⊢ ∀ (b : α), (single a 1) b ≠ 0 → b ≠ a → (single a 1) b = 0
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
a : α
⊢ ∀ (b : α), (single a 1) b ≠ 0 → b ≠ a → (single a 1) b = 0

Tactic:
exact fun _ _ hba ↦ single_eq_of_ne hba

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

Goal state before:
pp: M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x

Tactic:
by_cases hR : (n : R) = 0

Goal state after:
case pos
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x

case neg
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f g : ι → R
s : Finset ι
h0 : ∀ i ∈ s, 0 ≤ f i
h1 : ∀ i ∈ s, f i ≤ g i
⊢ ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i

Tactic:
by
  induction s using Finset.cons_induction with
  | empty => simp
  | cons a s has ih =>
    simp only [prod_cons, forall_mem_cons] at h0 h1 ⊢
    have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
    gcongr
    exacts [prod_nonneg h0.2, h0.1.trans h1.1, h1.1, ih h0.2 h1.2]

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ (single (f a) (x a)) (f a) = x a

pp: case h₀
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ ∀ (b : α), x b ≠ 0 → b ≠ a → (single (f b) (x b)) (f a) = 0

pp: case h₁
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ x a = 0 → (single (f a) 0) (f a) = 0

Tactic:
single_eq_same

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ x a = x a

case h₀
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ ∀ (b : α), x b ≠ 0 → b ≠ a → (single (f b) (x b)) (f a) = 0

case h₁
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ x a = 0 → (single (f a) 0) (f a) = 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) m).support)
hm : m ≠ 0
⊢ f ⁻¹' {f a} ⊆ {a} ∧ (single (f a) m) (f a) = m

Tactic:
single_eq_same

Goal state after:
case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) m).support)
hm : m ≠ 0
⊢ f ⁻¹' {f a} ⊆ {a} ∧ m = m
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : β →₀ M
h : ∀ b ∉ Set.range f, x b = 0
i : β
hi : i ∈ ↑x.support
hc : i ∉ Set.range f
⊢ False

Tactic:
simp only [Finset.mem_coe, Finsupp.mem_support_iff, ne_eq] at hi

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : β →₀ M
h : ∀ b ∉ Set.range f, x b = 0
i : β
hc : i ∉ Set.range f
hi : ¬x i = 0
⊢ False
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : ∑ i ∈ s, g i = 0
i : ι
hi : i ∈ s
⊢ r i = 0

Tactic:
simpa [(sum_eq_zero_iff_of_nonneg hg).1 h i hi] using ht i hi

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
⊢ ∏ x ∈ s, f x = (∏ x ∈ s with f x = 1, f x) * ∏ x ∈ s with f x ≠ 1, f x

Tactic:
rw [← prod_union, filter_union_filter_not_eq]

Goal state after:
ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
⊢ Disjoint ({x ∈ s | f x = 1}) ({x ∈ s | f x ≠ 1})
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
i : ι
⊢ (∃ a ∈ l.support, a.fst = i) ↔ (l.split i).support ≠ ∅

Tactic:
← Finset.nonempty_iff_ne_empty,

Goal state after:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
i : ι
⊢ (∃ a ∈ l.support, a.fst = i) ↔ (l.split i).support.Nonempty
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : α
s : Set α
h : single a 1 ∈ span R ((fun x ↦ single x 1) '' s)
⊢ a ∈ s

Tactic:
← Finsupp.supported_eq_span_single,

Goal state after:
α : Type u_1
R : Type u_5
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : α
s : Set α
h : single a 1 ∈ supported R R s
⊢ a ∈ s
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
⊢ p (∏ᶠ (i : α), f i)

Tactic:
by
  rw [finprod]
  split_ifs
  exacts [Finset.prod_induction _ _ hp₁ hp₀ fun i _ => hp₂ _, hp₀]

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

Goal state before:
pp: case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this✝ : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
this : (single (f x) (l x)) (f x) = 0
⊢ l x = 0 x

pp: case pos.h₀
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this✝ : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
this : (l.sum fun a₁ b ↦ (single (f a₁) b) (f x)) = 0
⊢ ∀ (b : α), l b ≠ 0 → b ≠ x → (single (f b) (l b)) (f x) = 0

pp: case pos.h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this✝ : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
this : (l.sum fun a₁ b ↦ (single (f a₁) b) (f x)) = 0
⊢ l x = 0 → (single (f x) 0) (f x) = 0

Tactic:
single_eq_same

Goal state after:
case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this✝ : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
this : l x = 0
⊢ l x = 0 x

case pos.h₀
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this✝ : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
this : (l.sum fun a₁ b ↦ (single (f a₁) b) (f x)) = 0
⊢ ∀ (b : α), l b ≠ 0 → b ≠ x → (single (f b) (l b)) (f x) = 0

case pos.h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this✝ : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
this : (l.sum fun a₁ b ↦ (single (f a₁) b) (f x)) = 0
⊢ l x = 0 → (single (f x) 0) (f x) = 0
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
m : ℕ
x : α
u : Fin m → α
⊢ vecTail (vecCons x u) = u

Tactic:
ext
  simp [vecTail]

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
h : p ≠ Fin.last n
x : { x // x ≠ p }
⊢ (finSuccAboveEquiv p).symm x = (p.castLT ⋯).predAbove ↑x

Tactic:
by
  rw [← Option.some_inj]
  simpa [finSuccAboveEquiv] using finSuccEquiv'_ne_last_apply h x.property

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
b : Fin n
⊢ #(Iic b) = ↑b + 1

Tactic:
rw [← Nat.card_Iic b, ← map_valEmbedding_Iic, card_map]

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

Goal state before:
pp: n✝ n : ℕ
inst✝ : NeZero n
x✝ : Fin n
a : ℕ
ha : a < n
⊢ n % n = 0

pp: n✝ n : ℕ
inst✝ : NeZero n
x✝ : Fin n
a : ℕ
ha : a < n
⊢ ↑⟨a, ha⟩ ≤ n

Tactic:
Nat.mod_self

Goal state after:
n✝ n : ℕ
inst✝ : NeZero n
x✝ : Fin n
a : ℕ
ha : a < n
⊢ 0 = 0

n✝ n : ℕ
inst✝ : NeZero n
x✝ : Fin n
a : ℕ
ha : a < n
⊢ ↑⟨a, ha⟩ ≤ n
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
⊢ ↑(a - 1) = if a = 0 then n else ↑a - 1

Tactic:
cases n
  · simp
  split_ifs with h
  · simp [h]
  exact val_sub_one_of_ne_zero h

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

Goal state before:
pp: case mpr.refine_3
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
f : ι →₀ R
⊢ ((fun y ↦ single default ⋯.choose) ((fun f ↦ f default • x) f)) default = f default

pp: case mpr.refine_4
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y : M
⊢ (fun f ↦ f default • x) ((fun y ↦ single default ⋯.choose) y) = y

Tactic:
· refine smul_left_injective _ nz ?_
      simp only [Finsupp.single_eq_same]
      exact (w (f default • x)).choose_spec

Goal state after:
case mpr.refine_4
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y : M
⊢ (fun f ↦ f default • x) ((fun y ↦ single default ⋯.choose) y) = y
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x y : ℕ∞
h : x ≠ 0
⊢ 1 ≤ x ^ y

Tactic:
exact one_le_epow h

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr
x y z : ℕ∞
y_0 : y ≠ 0
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
rcases eq_or_ne z 0 with z_0 | z_0

Goal state after:
case inr.inl
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z = 0
⊢ x ^ (y * z) = (x ^ y) ^ z

case inr.inr
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
⊢ x ^ (y * z) = (x ^ y) ^ z
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ a ≡ b [PMOD p] ↔ ∃ i, i < n ∧ a - i • p ≡ b [PMOD n • p]

Tactic:
modEq_comm (b := b)

Goal state after:
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ b ≡ a [PMOD p] ↔ ∃ i, i < n ∧ b ≡ a - i • p [PMOD n • p]
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : MulAction G R
inst✝² : SMul G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv : LinearIndependent R v
w : ι → G
⊢ LinearIndependent R (w • v)

Tactic:
by
  rw [linearIndependent_iff''ₛ] at hv ⊢
  intro s g₁ g₂ hgs hsum i
  refine (Group.isUnit (w i)).smul_left_cancel.mp ?_
  refine hv s (fun i ↦ w i • g₁ i) (fun i ↦ w i • g₂ i) (fun i hi ↦ ?_) ?_ i
  · simp_rw [hgs i hi]
  · simpa only [smul_assoc, smul_comm] using! hsum

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b c : ℕ
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

Tactic:
rcases eq_zero_or_pos a with rfl | ha0
  · simp [zero_pow_eq]; split_ifs <;> simp
  rcases Nat.eq_or_lt_of_le ha0 with rfl | ha1
  · simp
  rcases eq_zero_or_pos b with rfl | hb0
  · simp
  rcases lt_or_ge c b with h | h
  · rw [mod_eq_of_lt, mod_eq_of_lt h]
    rwa [Nat.sub_lt_sub_iff_right (one_le_pow c a ha0), Nat.pow_lt_pow_iff_right ha1]
  · suffices a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1) by
      rw [← Nat.sub_add_cancel h, add_mod_right, this, add_mod, mul_mod, mod_self,
        mul_zero, zero_mod, zero_add, mod_mod, pow_sub_one_mod_pow_sub_one]
    rw [← Nat.add_sub_assoc (one_le_pow (c - b) a ha0), ← mul_add_one, pow_add,
      Nat.sub_add_cancel (one_le_pow b a ha0)]

Goal state after: