awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Field.TransferInstance
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
q : ℚ
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (↑q : α) : β) ((↑q : β) : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Field.ULift
Goal:
α : Type u
inst : NNRatCast α
q : ℚ≥0
⊢ Eq (α := ULift.{u_1, u} α) { down := (↑q : α) } (↑q : ULift α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.ULift
Goal:
α : Type u
inst : NNRatCast α
q : ℚ≥0
⊢ Eq.{u + 1} (α := α) (down.{u_1, u} (↑q : ULift α)) (↑q : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.ULift
Goal:
α : Type u
inst : RatCast α
q : ℚ
⊢ Eq (α := ULift.{u_1, u} α) { down := (↑q : α) } (↑q : ULift α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.ULift
Goal:
α : Type u
inst : RatCast α
q : ℚ
⊢ Eq.{u + 1} (α := α) (down.{u_1, u} (↑q : ULift α)) (↑q : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.ZMod
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
h : a ≠ 0
obtain : ∀ (k : ℕ) (h : Ne (α := ZMod p) (↑k : ZMod p) 0), HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)⁻¹ = 1
⊢ a * a⁻¹ = 1

Tactic:
obtain ⟨k, rfl⟩ := natCast_zmod_surjective a

Premises used: ZMod.natCast_zmod_surjective, rfl
-- Module: Mathlib.Algebra.Field.ZMod
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
h : Ne (α := ZMod p) (↑k : ZMod p) 0
h₁ : k.Coprime p
⊢ HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)⁻¹ = 1

Tactic:
apply coe_mul_inv_eq_one

Premises used: ZMod.coe_mul_inv_eq_one
-- Module: Mathlib.Algebra.Field.ZMod
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
h : Ne (α := ZMod p) (↑k : ZMod p) 0
h₁ : p.Coprime k
⊢ k.Coprime p

Tactic:
apply Nat.Coprime.symm

Premises used: Nat.Coprime.symm
-- Module: Mathlib.Algebra.Field.ZMod
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
h : Ne (α := ZMod p) (↑k : ZMod p) 0
h₁ : ¬p ∣ k
h₂ h₃ h₄ h₅ : ¬Eq (α := ZMod p) (↑k : ZMod p) 0
⊢ p.Coprime k

Tactic:
rwa [Nat.Prime.coprime_iff_not_dvd Fact.out, ← CharP.cast_eq_zero_iff (ZMod p)]

Premises used: ZMod, CharP.cast_eq_zero_iff, Nat.Prime.coprime_iff_not_dvd, Fact.out
-- Module: Mathlib.Algebra.Field.ZMod
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsDomain (ZMod p)

Tactic:
constructor
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
⊢ HasFiniteMulSupport.{u_1, u_2} (α := α) (M := M) 1

Tactic:
simp [HasFiniteMulSupport]

Premises used: Function.HasFiniteMulSupport
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
N : Type u_3
inst_1 : One N
g : M → N
f : α → M
hf : HasFiniteMulSupport f
hg : g 1 = 1
⊢ HasFiniteMulSupport.{u_1, u_3} (M := N) fun (a : α) ↦ g (f a)

Tactic:
hf.subset <| mulSupport_comp_subset hg f

Premises used: Function.mulSupport_comp_subset, Set.Finite.subset, Function.HasFiniteMulSupport
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
N : Type u_3
inst_1 : One N
g : M → N
f : α → M
hf : HasFiniteMulSupport f
hg : g 1 = 1
⊢ HasFiniteMulSupport (g ∘ f)

Tactic:
hf.subset <| mulSupport_comp_subset hg f

Premises used: Function.mulSupport_comp_subset, Set.Finite.subset, Function.HasFiniteMulSupport
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
M' : Type u_3
inst_1 : One M'
f : α → M × M'
hf : HasFiniteMulSupport f
⊢ HasFiniteMulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ (f a).1

Tactic:
hf.comp rfl

Premises used: Function.HasFiniteMulSupport.comp, rfl
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
M' : Type u_3
inst_1 : One M'
f : α → M × M'
hf : HasFiniteMulSupport f
⊢ HasFiniteMulSupport.{u_1, u_3} (M := M') fun (a : α) ↦ (f a).2

Tactic:
hf.comp rfl

Premises used: Function.HasFiniteMulSupport.comp, rfl
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
M' : Type u_3
inst_1 : One M'
f : α → M
g : α → M'
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
rw : (mulSupport f ∪ mulSupport g).Finite
⊢ Set.Finite.{u_1} (α := α) (mulSupport (M := M × M') fun (a : α) ↦ (f a, g a))

Tactic:
rw [mulSupport_prodMk f g]

Premises used: Function.mulSupport_prodMk
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
M' : Type u_3
inst_1 : One M'
f : α → M
g : α → M'
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
⊢ (mulSupport f ∪ mulSupport g).Finite

Tactic:
hf.union hg

Premises used: Set.Finite.union
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
M' : Type u_3
inst_1 : One M'
f : α → M
g : α → M'
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
⊢ (mulSupport f ∪ mulSupport g).Finite

Tactic:
exact hf.union hg

Premises used: Set.Finite.union
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_3
inst : MulOneClass M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ HasFiniteMulSupport (f * g)

Tactic:
(hf.union hg).subset <| mulSupport_mul ..

Premises used: Set.Finite.union, Set.Finite.subset, Function.HasFiniteMulSupport, Function.mulSupport_mul
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_3
inst : DivisionMonoid M
f : α → M
hf : HasFiniteMulSupport f
⊢ HasFiniteMulSupport f⁻¹

Tactic:
hf.comp inv_one

Premises used: inv_one, Function.HasFiniteMulSupport.comp
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_3
inst : CommMonoid M
ι : Type u_4
f : ι → α → M
hf : ∀ (i : ι), HasFiniteMulSupport (f i)
s : Finset ι
⊢ HasFiniteMulSupport.{u_1, u_3} (M := M) fun (a : α) ↦ ∏ i ∈ s, f i a

Tactic:
(s.finite_toSet.biUnion fun i _ ↦ hf i).subset <| s.mulSupport_prod f

Premises used: Set.Finite.subset, Finset.mulSupport_prod, Finset.finite_toSet, Set.Finite.biUnion, Function.HasFiniteMulSupport
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_3
inst : DivisionMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ HasFiniteMulSupport (f / g)

Tactic:
(hf.union hg).subset <| mulSupport_div ..

Premises used: Set.Finite.union, Function.mulSupport_div, Set.Finite.subset, Function.HasFiniteMulSupport
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
f : α → M
hf : HasFiniteMulSupport f
n : ℕ
⊢ HasFiniteMulSupport (f ^ n)

Tactic:
hf.comp (one_pow n)

Premises used: one_pow, Function.HasFiniteMulSupport.comp
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_3
inst : DivisionMonoid M
f : α → M
hf : HasFiniteMulSupport f
n : ℤ
⊢ HasFiniteMulSupport (f ^ n)

Tactic:
hf.comp (one_zpow n)

Premises used: Function.HasFiniteMulSupport.comp, one_zpow
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : LinearOrder M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ HasFiniteMulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ Max.max (f a) (g a)

Tactic:
(hf.union hg).subset <| mulSupport_max ..

Premises used: Set.Finite.union, Set.Finite.subset, Function.mulSupport_max, Function.HasFiniteMulSupport
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : LinearOrder M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ HasFiniteMulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ Min.min (f a) (g a)

Tactic:
(hf.union hg).subset <| mulSupport_min ..

Premises used: Set.Finite.union, Set.Finite.subset, Function.mulSupport_min, Function.HasFiniteMulSupport
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : SemilatticeSup M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ HasFiniteMulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ f a ⊔ g a

Tactic:
(hf.union hg).subset <| mulSupport_sup ..

Premises used: Set.Finite.union, Set.Finite.subset, Function.HasFiniteMulSupport, Function.mulSupport_sup
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : SemilatticeInf M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ HasFiniteMulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ f a ⊓ g a

Tactic:
(hf.union hg).subset <| mulSupport_inf ..

Premises used: Set.Finite.union, Set.Finite.subset, Function.HasFiniteMulSupport, Function.mulSupport_inf
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : ConditionallyCompleteLattice M
ι : Sort u_3
inst_2 : Nonempty ι
inst_3 : Finite ι
f : ι → α → M
hf : ∀ (i : ι), HasFiniteMulSupport (f i)
⊢ HasFiniteMulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ ⨆ (i : ι), f i a

Tactic:
(Set.finite_iUnion hf).subset <| mulSupport_iSup f

Premises used: Set.finite_iUnion, Function.mulSupport_iSup, Set.Finite.subset, Function.HasFiniteMulSupport
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : ConditionallyCompleteLattice M
ι : Sort u_3
inst_2 : Nonempty ι
inst_3 : Finite ι
f : ι → α → M
hf : ∀ (i : ι), HasFiniteMulSupport (f i)
⊢ HasFiniteMulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ ⨅ (i : ι), f i a

Tactic:
(Set.finite_iUnion hf).subset <| mulSupport_iInf f

Premises used: Set.finite_iUnion, Set.Finite.subset, Function.mulSupport_iInf, Function.HasFiniteMulSupport
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
ι : Type u_3
inst_1 : Finite α
f : ι → α → M
hf : ∀ (a : α), Set.Finite.{u_3} (α := ι) (mulSupport.{u_3, u_2} (M := M) fun (x : ι) ↦ f x a)
⊢ (mulSupport f).Finite

Tactic:
(Set.finite_iUnion hf).subset fun i hi ↦ ?_

Premises used: Set.finite_iUnion, Set.Finite.subset
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
ι : Type u_3
inst_1 : Finite α
f : ι → α → M
hf : ∀ (a : α), Set.Finite.{u_3} (α := ι) (mulSupport.{u_3, u_2} (M := M) fun (x : ι) ↦ f x a)
refine :
  ∀ (i : ι) (hi : i ∈ mulSupport f),
    Membership.mem (γ := Set ι) (⋃ (i : α), mulSupport.{u_3, u_2} (M := M) fun (x : ι) ↦ f x i) i
⊢ (mulSupport f).Finite

Tactic:
refine (Set.finite_iUnion hf).subset fun i hi ↦ ?_

Premises used: Set.finite_iUnion, Set.Finite.subset
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
ι : Type u_3
inst_1 : Finite α
f : ι → α → M
hf : ∀ (a : α), Set.Finite.{u_3} (α := ι) (mulSupport.{u_3, u_2} (M := M) fun (x : ι) ↦ f x a)
i : ι
hi : i ∈ mulSupport f
simp : ∀ (hi : f i ≠ 1), ∃ (i_1 : α), f i i_1 ≠ 1
⊢ Membership.mem (γ := Set ι) (⋃ (i : α), mulSupport.{u_3, u_2} (M := M) fun (x : ι) ↦ f x i) i

Tactic:
simp only [mem_mulSupport, Set.mem_iUnion] at hi ⊢

Premises used: Set.mem_iUnion, Function.mem_mulSupport
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
ι : Type u_3
inst_1 : Finite α
f : ι → α → M
hf : ∀ (a : α), Set.Finite.{u_3} (α := ι) (mulSupport.{u_3, u_2} (M := M) fun (x : ι) ↦ f x a)
i : ι
hi : f i ≠ 1
⊢ ∃ (i_1 : α), f i i_1 ≠ 1

Tactic:
ne_iff.mp hi

Premises used: Function.ne_iff, Iff.mp
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
ι : Type u_3
inst_1 : Finite α
f : ι → α → M
hf : ∀ (a : α), Set.Finite.{u_3} (α := ι) (mulSupport.{u_3, u_2} (M := M) fun (x : ι) ↦ f x a)
i : ι
hi : f i ≠ 1
⊢ ∃ (i_1 : α), f i i_1 ≠ 1

Tactic:
exact ne_iff.mp hi

Premises used: Function.ne_iff, Iff.mp
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : SemilatticeSup M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
⊢ Set.Finite.{u_1} (α := α) (mulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ s.sup' hs fun (x : ι) ↦ f x a)

Tactic:
(s.finite_toSet.biUnion hf).subset fun a ha ↦ ?_

Premises used: Set.Finite.subset, Finset.finite_toSet, Set.Finite.biUnion
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : SemilatticeSup M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
refine :
  ∀ (a : α)
    (ha : Membership.mem (γ := Set α) (mulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ s.sup' hs fun (x : ι) ↦ f x a) a),
    Membership.mem (γ := Set α) (⋃ i ∈ (↑s : Set ι), mulSupport (f i)) a
⊢ Set.Finite.{u_1} (α := α) (mulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ s.sup' hs fun (x : ι) ↦ f x a)

Tactic:
refine (s.finite_toSet.biUnion hf).subset fun a ha ↦ ?_

Premises used: Set.Finite.subset, Finset.finite_toSet, Set.Finite.biUnion
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : SemilatticeSup M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
a : α
ha : Membership.mem (γ := Set α) (mulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ s.sup' hs fun (x : ι) ↦ f x a) a
simp : ∀ (ha : Ne.{u_2 + 1} (α := M) (s.sup' hs fun (x : ι) ↦ f x a) 1), ∃ i ∈ s, f i a ≠ 1
⊢ Membership.mem (γ := Set α) (⋃ i ∈ (↑s : Set ι), mulSupport (f i)) a

Tactic:
simp only [mem_mulSupport, SetLike.mem_coe, Set.mem_iUnion, exists_prop] at ha ⊢

Premises used: Set.mem_iUnion, Function.mem_mulSupport, exists_prop, SetLike.mem_coe
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : SemilatticeSup M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
a : α
ha : Ne.{u_2 + 1} (α := M) (s.sup' hs fun (x : ι) ↦ f x a) 1
contrapose! : ∀ (ha : ∀ (i : ι) (_ : i ∈ s), f i a = 1), Eq.{u_2 + 1} (α := M) (s.sup' hs fun (x : ι) ↦ f x a) 1
⊢ ∃ i ∈ s, f i a ≠ 1

Tactic:
contrapose! ha
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : SemilatticeSup M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
a : α
ha : ∀ (i : ι) (_ : i ∈ s), f i a = 1
⊢ Eq.{u_2 + 1} (α := M) (s.sup' hs fun (x : ι) ↦ f x a) 1

Tactic:
Finset.sup'_eq_of_forall hs (fun x ↦ f x a) ha

Premises used: Finset.sup'_eq_of_forall
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : SemilatticeSup M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
a : α
ha : ∀ (i : ι) (_ : i ∈ s), f i a = 1
⊢ Eq.{u_2 + 1} (α := M) (s.sup' hs fun (x : ι) ↦ f x a) 1

Tactic:
exact Finset.sup'_eq_of_forall hs (fun x ↦ f x a) ha

Premises used: Finset.sup'_eq_of_forall
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : SemilatticeInf M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
⊢ Set.Finite.{u_1} (α := α) (mulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ s.inf' hs fun (x : ι) ↦ f x a)

Tactic:
(s.finite_toSet.biUnion hf).subset fun a ha ↦ ?_

Premises used: Set.Finite.subset, Finset.finite_toSet, Set.Finite.biUnion
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : SemilatticeInf M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
refine :
  ∀ (a : α)
    (ha : Membership.mem (γ := Set α) (mulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ s.inf' hs fun (x : ι) ↦ f x a) a),
    Membership.mem (γ := Set α) (⋃ i ∈ (↑s : Set ι), mulSupport (f i)) a
⊢ Set.Finite.{u_1} (α := α) (mulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ s.inf' hs fun (x : ι) ↦ f x a)

Tactic:
refine (s.finite_toSet.biUnion hf).subset fun a ha ↦ ?_

Premises used: Set.Finite.subset, Finset.finite_toSet, Set.Finite.biUnion
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : SemilatticeInf M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
a : α
ha : Membership.mem (γ := Set α) (mulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ s.inf' hs fun (x : ι) ↦ f x a) a
simp : ∀ (ha : Ne.{u_2 + 1} (α := M) (s.inf' hs fun (x : ι) ↦ f x a) 1), ∃ i ∈ s, f i a ≠ 1
⊢ Membership.mem (γ := Set α) (⋃ i ∈ (↑s : Set ι), mulSupport (f i)) a

Tactic:
simp only [mem_mulSupport, SetLike.mem_coe, Set.mem_iUnion, exists_prop] at ha ⊢

Premises used: Set.mem_iUnion, Function.mem_mulSupport, exists_prop, SetLike.mem_coe
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : SemilatticeInf M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
a : α
ha : Ne.{u_2 + 1} (α := M) (s.inf' hs fun (x : ι) ↦ f x a) 1
contrapose! : ∀ (ha : ∀ (i : ι) (_ : i ∈ s), f i a = 1), Eq.{u_2 + 1} (α := M) (s.inf' hs fun (x : ι) ↦ f x a) 1
⊢ ∃ i ∈ s, f i a ≠ 1

Tactic:
contrapose! ha
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : SemilatticeInf M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
a : α
ha : ∀ (i : ι) (_ : i ∈ s), f i a = 1
⊢ Eq.{u_2 + 1} (α := M) (s.inf' hs fun (x : ι) ↦ f x a) 1

Tactic:
Finset.inf'_eq_of_forall hs (fun x ↦ f x a) ha

Premises used: Finset.inf'_eq_of_forall
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
inst_1 : SemilatticeInf M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
a : α
ha : ∀ (i : ι) (_ : i ∈ s), f i a = 1
⊢ Eq.{u_2 + 1} (α := M) (s.inf' hs fun (x : ι) ↦ f x a) 1

Tactic:
exact Finset.inf'_eq_of_forall hs (fun x ↦ f x a) ha

Premises used: Finset.inf'_eq_of_forall
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
β : Type u_3
f : β → M
g : α → β
hg : Injective g
hf : HasFiniteMulSupport f
⊢ HasFiniteMulSupport (f ∘ g)

Tactic:
Set.Finite.of_injOn ?_ (Set.injOn_of_injective hg) hf

Premises used: Set.Finite.of_injOn, Function.HasFiniteMulSupport, Set.injOn_of_injective
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
β : Type u_3
f : β → M
g : α → β
hg : Injective g
hf : HasFiniteMulSupport f
refine : Set.MapsTo g (mulSupport (f ∘ g)) (mulSupport f)
⊢ HasFiniteMulSupport (f ∘ g)

Tactic:
refine Set.Finite.of_injOn ?_ (Set.injOn_of_injective hg) hf

Premises used: Set.Finite.of_injOn, Set.injOn_of_injective
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
β : Type u_3
f : β → M
g : α → β
hg : Injective g
hf : HasFiniteMulSupport f
⊢ Set.MapsTo g (mulSupport (f ∘ g)) (mulSupport f)

Tactic:
grind [Set.mapsTo_iff_subset_preimage, Function.mulSupport]

Premises used: Set.mapsTo_iff_subset_preimage, Function.mulSupport
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
β : Type u_3
f : β → M
g : α → β
hg : Injective g
hf : HasFiniteMulSupport f
⊢ HasFiniteMulSupport.{u_1, u_2} (M := M) fun (a : α) ↦ f (g a)

Tactic:
hf.comp_of_injective hg

Premises used: Function.HasFiniteMulSupport.comp_of_injective
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
β : Type u_3
f : β → M
g : α → β
inst_1 : One β
hfg : HasFiniteMulSupport (f ∘ g)
h : f 1 = 1
hf : Injective f
⊢ HasFiniteMulSupport g

Tactic:
Set.Finite.subset hfg fun _ ha ↦ Set.mem_setOf.mpr fun H ↦ Set.mem_setOf.mp ha ?_

Premises used: Iff.mpr, Set.Finite.subset, Set.mem_setOf, Iff.mp, Function.HasFiniteMulSupport
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
β : Type u_3
f : β → M
g : α → β
inst_1 : One β
hfg : HasFiniteMulSupport (f ∘ g)
h : f 1 = 1
hf : Injective f
refine : ∀ (x : α) (ha : x ∈ mulSupport g) (H : (f ∘ g) x = 1), g x = 1
⊢ HasFiniteMulSupport g

Tactic:
refine Set.Finite.subset hfg fun _ ha ↦ Set.mem_setOf.mpr fun H ↦ Set.mem_setOf.mp ha ?_
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_2
inst : One M
β : Type u_3
f : β → M
g : α → β
inst_1 : One β
hfg : HasFiniteMulSupport (f ∘ g)
h : f 1 = 1
hf : Injective f
x : α
ha : x ∈ mulSupport g
H : (f ∘ g) x = 1
⊢ g x = 1

Tactic:
grind
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_4
inst : Monoid M
f : α → M
g : α → ℕ
hg : HasFiniteSupport g
a : α
ha : Membership.mem (γ := Set α) (mulSupport.{u_1, u_4} (M := M) fun (a : α) ↦ f a ^ g a) a
contrapose! : ∀ (ha : a ∉ support g), a ∉ mulSupport.{u_1, u_4} (M := M) fun (a : α) ↦ f a ^ g a
⊢ a ∈ support g

Tactic:
contrapose! ha
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_4
inst : Monoid M
f : α → M
g : α → ℕ
hg : HasFiniteSupport g
a : α
ha : a ∉ support g
⊢ a ∉ mulSupport.{u_1, u_4} (M := M) fun (a : α) ↦ f a ^ g a

Tactic:
simp_all
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_4
inst : MulZeroClass M
f : α → M
hf : HasFiniteSupport f
g : α → M
⊢ HasFiniteSupport (f * g)

Tactic:
Set.Finite.subset hf fun _ ha ↦ support_mul_subset_left f g ha

Premises used: Function.HasFiniteSupport, Function.support_mul_subset_left, Set.Finite.subset
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
M : Type u_4
inst : MulZeroClass M
f g : α → M
hg : HasFiniteSupport g
⊢ HasFiniteSupport (f * g)

Tactic:
Set.Finite.subset hg fun _ ha ↦ support_mul_subset_right f g ha

Premises used: Function.support_mul_subset_right, Function.HasFiniteSupport, Set.Finite.subset
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ (Function.support (M := ℕ) fun (x : α) ↦ count x s) ⊆ (↑s.toFinset : Set α)

Tactic:
simp
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero M
inst_1 : Zero R
inst_2 : SMulWithZero R M
f : α → R
hf : HasFiniteSupport f
g : α → M
⊢ HasFiniteSupport (f • g)

Tactic:
Set.Finite.subset hf fun _ ha ↦ support_smul_subset_left f g ha

Premises used: Function.support_smul_subset_left, Function.HasFiniteSupport, Set.Finite.subset
-- Module: Mathlib.Algebra.FiniteSupport.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero M
inst_1 : SMulZeroClass R M
f : α → R
g : α → M
hg : HasFiniteSupport g
⊢ HasFiniteSupport (f • g)

Tactic:
Set.Finite.subset hg fun _ ha ↦ support_smul_subset_right f g ha

Premises used: Function.HasFiniteSupport, Function.support_smul_subset_right, Set.Finite.subset
-- Module: Mathlib.Algebra.FiniteSupport.Defs
Goal:
α : Type u_1
M : Type u_2
inst : One M
⊢ HasFiniteMulSupport.{u_1, u_2} (M := M) fun (x : α) ↦ 1

Tactic:
simp [HasFiniteMulSupport]

Premises used: Function.HasFiniteMulSupport
-- Module: Mathlib.Algebra.FiveLemma
Goal:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst : Group M₁
inst_1 : Group M₂
inst_2 : Group M₃
inst_3 : Group M₄
inst_4 : Group N₁
inst_5 : Group N₂
inst_6 : Group N₃
inst_7 : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₂ : Function.MulExact.{u_2, u_3, u_4} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
hg₁ : Function.MulExact.{u_6, u_7, u_8} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hg₂ : Function.MulExact.{u_7, u_8, u_9} (M := N₂) (N := N₃) (P := N₄) (⇑g₂ : (a : N₂) → N₃) (⇑g₃ : (a : N₃) → N₄)
hi₁ : Function.Surjective.{u_1 + 1, u_6 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
hi₃ : Function.Surjective.{u_3 + 1, u_8 + 1} (α := M₃) (β := N₃) (⇑i₃ : (a : M₃) → N₃)
hi₄ : Function.Injective.{u_4 + 1, u_9 + 1} (α := M₄) (β := N₄) (⇑i₄ : (a : M₄) → N₄)
x : N₂
obtain :
  ∀ (y : M₃) (hy : Eq.{u_8 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) y : N₃) ((g₂ : (a : N₂) → N₃) x : N₃)),
    ∃ (a : M₂), (i₂ : (a : M₂) → N₂) a = x
⊢ ∃ (a : M₂), (i₂ : (a : M₂) → N₂) a = x

Tactic:
obtain ⟨y, hy⟩ := hi₃ (g₂ x)

Premises used: DFunLike.coe